Free-Style Theorem Proving

g Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Simon J. Ambler, Roy L. Crole, Alberto Momigliano Efficient Reasoning about Executable Specifications in Coq . . . . . . . . . . . . . . 31 Gilles Barthe, Pierre Courtieu Verified Bytecode Model Checkers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 David Basin, Stefan Friedrich, Marek Gawkowski The 5 Colour Theorem in Isabelle/Isar. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 Gertrud Bauer, Tobias Nipkow Type-Theoretic Functional Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 Yves Bertot, Venanzio Capretta, Kuntal Das Barman A Proposal for a Formal OCL Semantics in Isabelle/HOL . . . . . . . . . . . . . . . 99 Achim D. Brucker, Burkhart Wolff Explicit Universes for the Calculus of Constructions . . . . . . . . . . . . . . . ...

• Type: Conference
• Year: 2002
• Where: TPHOL
• Authors: David Delahaye
• Keywords: Automated Reasoning, Colour Theorem, Tactical Theorem Proving, TPHOL 2002, Type-Theoretic Functional Semantics