Proof Pearl: Mechanizing the Textbook Proof of Huffman’s Algorithm Jasmin Christian Blanchette OriginalPaper 13 February 2009 Pages: 1 - 18
An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps Jean-François Dufourd OriginalPaper 06 March 2009 Pages: 19 - 51
On Process Equivalence = Equation Solving in CCS Raúl MonroyAlan BundyIan Green OriginalPaper 20 March 2009 Pages: 53 - 80
Formalization and Implementation of Modern SAT Solvers Filip Marić OriginalPaper 04 April 2009 Pages: 81 - 119
