Theorem Proving in Higher Order Logics

Invited Talks.- Formal Methods at NASA Langley.- Higher Order Unification 30 Years Later.- Regular Papers.- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.- Efficient Reasoning about Executable Specifications in Coq.- Verified Bytecode Model Checkers.- The 5 Colour Theorem in Isabelle/Isar.- Type-Theoretic Functional Semantics.- A Proposal for a Formal OCL Semantics in Isabelle/HOL.- Explicit Universes for the Calculus of Constructions.- Formalised Cut Admissibility for Display Logic.- Formalizing the Trading Theorem for the Classification of Surfaces.- Free-Style Theorem Proving.- A Comparison of Two Proof Critics: Power vs. Robustness.- Two-Level Meta-reasoning in Coq.- PuzzleTool: An Example of Programming Computation and Deduction.- A Formal Approach to Probabilistic Termination.- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm.- Quotient Types: A Modular Approach.- Sequent Schema for Derived Rules.- Algebraic Structures and Dependent Records.- Proving the Equivalence of Microstep and Macrostep Semantics.- Weakest Precondition for General Recursive Programs Formalized in Coq.

Includes supplementary material: sn.pub/extras