Abstract is missing.
- Twenty Years of Theorem Proving for HOLs Past, Present and FutureMike Gordon. 1-5 [doi]
- Will This Be Formal?Steven P. Miller. 6-11 [doi]
- A Short Presentation of CoqYves Bertot. 12-16 [doi]
- An ACL2 TutorialMatt Kaufmann, J. Strother Moore. 17-21 [doi]
- A Brief Overview of PVSSam Owre, Natarajan Shankar. 22-27 [doi]
- A Brief Overview of HOL4Konrad Slind, Michael Norrish. 28-32 [doi]
- The Isabelle FrameworkMakarius Wenzel, Lawrence C. Paulson, Tobias Nipkow. 33-38 [doi]
- A Compiled Implementation of Normalization by EvaluationKlaus Aehlig, Florian Haftmann, Tobias Nipkow. 39-54 [doi]
- LCF-Style Propositional Simplification with BDDs and SAT SolversHasan Amjad. 55-70 [doi]
- Nominal Inversion PrinciplesStefan Berghofer, Christian Urban. 71-85 [doi]
- Canonical Big OperatorsYves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca. 86-101 [doi]
- A Type of Partial Recursive FunctionsAna Bove, Venanzio Capretta. 102-117 [doi]
- Formal Reasoning About Causality AnalysisJens Brandt, Klaus Schneider. 118-133 [doi]
- Imperative Functional Programming with Isabelle/HOLLukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews. 134-149 [doi]
- HOL-Boogie - An Interactive Prover for the Boogie Program-VerifierSascha Böhme, K. Rustan M. Leino, Burkhart Wolff. 150-166 [doi]
- Secure Microkernels, State Monads and Scalable RefinementDavid Cock, Gerwin Klein, Thomas Sewell. 167-182 [doi]
- Certifying a Termination Criterion Based on Graphs, without GraphsPierre Courtieu, Julien Forest, Xavier Urbain. 183-198 [doi]
- Lightweight SeparationHolger Gast. 199-214 [doi]
- Real Number Calculations and Theorem ProvingDavid R. Lester. 215-229 [doi]
- A Formalized Theory for Verifying Stability and Convergence of Automata in PVSSayan Mitra, K. Mani Chandy. 230-245 [doi]
- Certified Exact Transcendental Real Number Computation in CoqRussell O Connor. 246-261 [doi]
- Formalizing Soundness of Contextual EffectsPolyvios Pratikakis, Jeffrey S. Foster, Michael Hicks, Iulian Neamtiu. 262-277 [doi]
- First-Class Type ClassesMatthieu Sozeau, Nicolas Oury. 278-293 [doi]
- Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOLDaniel Wasserrab, Andreas Lochbihler. 294-309 [doi]
- Proof Pearl: Revisiting the Mini-rubik in CoqLaurent Théry. 310-319 [doi]