15. TPHOLs 2002: Hampton, VA, USA

Victor Carreño, César Muñoz, Sofiène Tahar (Eds.): Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings. Lecture Notes in Computer Science 2410 Springer 2002, ISBN 3-540-44039-9

Invited Talks

Ricky W. Butler:
Formal Methods at NASA Langley. 1-2
Gérard P. Huet:
Higher Order Unification 30 Years Later. 3-12

Regular Papers

Simon Ambler, Roy L. Crole, Alberto Momigliano:
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. 13-30
Gilles Barthe, Pierre Courtieu:
Efficient Reasoning about Executable Specifications in Coq. 31-46
David A. Basin, Stefan Friedrich, Marek Gawkowski:
Verified Bytecode Model Checkers. 47-66
Gertrud Bauer, Tobias Nipkow:
The 5 Colour Theorem in Isabelle/Isar. 67-82
Yves Bertot, Venanzio Capretta, Kuntal Das Barman:
Type-Theoretic Functional Semantics. 83-98
Achim D. Brucker, Burkhart Wolff:
A Proposal for a Formal OCL Semantics in Isabelle/HOL. 99-114
Judicaël Courant:
Explicit Universes for the Calculus of Constructions. 115-130
Jeremy E. Dawson, Rajeev Goré:
Formalised Cut Admissibility for Display Logic. 131-147
Christophe Dehlinger, Jean-François Dufourd:
Formalizing the Trading Theorem for the Classification of Surfaces. 148-163
David Delahaye:
Free-Style Theorem Proving. 164-181
Louise A. Dennis, Alan Bundy:
A Comparison of Two Proof Critics: Power vs. Robustness. 182-197
Amy P. Felty:
Two-Level Meta-reasoning in Coq. 198-213
Michael J. C. Gordon:
PuzzleTool : An Example of Programming Computation and Deduction. 214-229
Joe Hurd:
A Formal Approach to Probabilistic Termination. 230-245
Micaela Mayero:
Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). 246-262
Aleksey Nogin:
Quotient Types: A Modular Approach. 263-280
Aleksey Nogin, Jason Hickey:
Sequent Schema for Derived Rules. 281-297
Virgile Prevosto, Damien Doligez, Thérèse Hardin:
Algebraic Structures and Dependent Records. 298-313
Klaus Schneider:
Proving the Equivalence of Microstep and Macrostep Semantics. 314-331
Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu:
Weakest Precondition for General Recursive Programs Formalized in Coq. 332-348