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
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
Last update Fri May 25 08:43:21 2012
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
