default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID15th TPHOLs 2002: Hampton, VA, USA
- Victor Carreño, César A. Muñoz, Sofiène Tahar:
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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2026-05-27 02:06 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
