Minimal from classical proofs. - Helmut Schwichtenberg; Christoph Senjak (Ann. Pure Appl. Log., 2013)

An Implementation of Deflate in Coq. - Christoph-Simon Senjak; Martin Hofmann 001 (FM, 2016)