Sciweavers

TPHOL
2002
IEEE

Free-Style Theorem Proving

13 years 10 months ago
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 . . . . . . . . . . . . . . . ...
David Delahaye
Added 16 Jul 2010
Updated 16 Jul 2010
Type Conference
Year 2002
Where TPHOL
Authors David Delahaye
Comments (0)