1. Proof Pearl: Mechanizing the Textbook Proof of Huffman’s Algorithm

   • Jasmin Christian Blanchette

   OriginalPaper 13 February 2009 Pages: 1 - 18

2. 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

3. On Process Equivalence = Equation Solving in CCS

   • Raúl Monroy
   • Alan Bundy
   • Ian Green

   OriginalPaper 20 March 2009 Pages: 53 - 80

4. Formalization and Implementation of Modern SAT Solvers

   • Filip Marić

   OriginalPaper 04 April 2009 Pages: 81 - 119