1. Preface

   OriginalPaper Pages: 195 - 196

2. On Equivalents of Well-Foundedness

   • Piotr Rudnicki
   • Andrzej Trybulec

   OriginalPaper Pages: 197 - 234

3. A Formal Proof of Sylow's Theorem

   • Florian Kammüller
   • Lawrence C. Paulson

   OriginalPaper Pages: 235 - 264

4. Formal Verification of a Partial-Order Reduction Technique for Model Checking

   • Ching-Tsun Chou
   • Doron Peled

   OriginalPaper Pages: 265 - 298

5. Type Inference Verified: Algorithm W in Isabelle/HOL

   • Wolfgang Naraschewski
   • Tobias Nipkow

   OriginalPaper Pages: 299 - 318

6. Certification of a Type Inference Tool for ML: Damas–Milner within Coq

   • Catherine Dubois
   • Valérie Ménissier-Morain

   OriginalPaper Pages: 319 - 346

7. A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions

   • M. Jaume

   OriginalPaper Pages: 347 - 371

8. Some Lambda Calculus and Type Theory Formalized

   • James McKinna
   • Robert Pollack

   OriginalPaper Pages: 373 - 409

9. Formalizing Synthetic Domain Theory

   • Bernhard Reus

   OriginalPaper Pages: 411 - 444

10. A Mechanization of Unity in PC-NQTHM-92

    • David M. Goldschlag

    OriginalPaper Pages: 445 - 498