Abstract is missing.
- Formal Methods at NASA LangleyRicky W. Butler. 1-2 [doi]
- Higher Order Unification 30 Years LaterGérard P. Huet. 3-12 [doi]
- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)InductionSimon Ambler, Roy L. Crole, Alberto Momigliano. 13-30 [doi]
- Efficient Reasoning about Executable Specifications in CoqGilles Barthe, Pierre Courtieu. 31-46 [doi]
- Verified Bytecode Model CheckersDavid A. Basin, Stefan Friedrich, Marek Gawkowski. 47-66 [doi]
- The 5 Colour Theorem in Isabelle/IsarGertrud Bauer, Tobias Nipkow. 67-82 [doi]
- Type-Theoretic Functional SemanticsYves Bertot, Venanzio Capretta, Kuntal Das Barman. 83-98 [doi]
- A Proposal for a Formal OCL Semantics in Isabelle/HOLAchim D. Brucker, Burkhart Wolff. 99-114 [doi]
- Explicit Universes for the Calculus of ConstructionsJudicaël Courant. 115-130 [doi]
- Formalised Cut Admissibility for Display LogicJeremy E. Dawson, Rajeev Goré. 131-147 [doi]
- Formalizing the Trading Theorem for the Classification of SurfacesChristophe Dehlinger, Jean-François Dufourd. 148-163 [doi]
- Free-Style Theorem ProvingDavid Delahaye. 164-181 [doi]
- A Comparison of Two Proof Critics: Power vs. RobustnessLouise A. Dennis, Alan Bundy. 182-197 [doi]
- Two-Level Meta-reasoning in CoqAmy P. Felty. 198-213 [doi]
- PuzzleTool : An Example of Programming Computation and DeductionMichael J. C. Gordon. 214-229 [doi]
- A Formal Approach to Probabilistic TerminationJoe Hurd. 230-245 [doi]
- Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm)Micaela Mayero. 246-262 [doi]
- Quotient Types: A Modular ApproachAleksey Nogin. 263-280 [doi]
- Sequent Schema for Derived RulesAleksey Nogin, Jason Hickey. 281-297 [doi]
- Algebraic Structures and Dependent RecordsVirgile Prevosto, Damien Doligez, Thérèse Hardin. 298-313 [doi]
- Proving the Equivalence of Microstep and Macrostep SemanticsKlaus Schneider. 314-331 [doi]
- Weakest Precondition for General Recursive Programs Formalized in CoqXingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu. 332-348 [doi]