A Formal Proof of Sylow's Theorem Florian KammüllerLawrence C. Paulson OriginalPaper Pages: 235 - 264
Formal Verification of a Partial-Order Reduction Technique for Model Checking Ching-Tsun ChouDoron Peled OriginalPaper Pages: 265 - 298
Type Inference Verified: Algorithm W in Isabelle/HOL Wolfgang NaraschewskiTobias Nipkow OriginalPaper Pages: 299 - 318
Certification of a Type Inference Tool for ML: Damas–Milner within Coq Catherine DuboisValérie Ménissier-Morain OriginalPaper Pages: 319 - 346
A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions M. Jaume OriginalPaper Pages: 347 - 371
Some Lambda Calculus and Type Theory Formalized James McKinnaRobert Pollack OriginalPaper Pages: 373 - 409
