15. TPHOLs 2002: Hampton, VA, USA

@proceedings{DBLP:conf/tphol/2002,
  editor    = {Victor Carre{\~n}o and
               C{\'e}sar Mu{\~n}oz and
               Sofi{\`e}ne Tahar},
  title     = {Theorem Proving in Higher Order Logics, 15th International Conference,
               TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2410},
  year      = {2002},
  isbn      = {3-540-44039-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Talks

• Ricky W. Butler:
  Formal Methods at NASA Langley. 1-2
  Electronic Edition (Springer LINK) BibTeX
• Gérard P. Huet:
  Higher Order Unification 30 Years Later. 3-12
  Electronic Edition (Springer LINK) BibTeX

Regular Papers

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