This book constitutes the refereed proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, held in Hampton, VA, USA in August 2002.
The 20 revised full papers presented together with 2 invited contributions were carefully reviewed and selected from 34 submissions. All current issues in HOL theorem proving and formal verification of software and hardware systems are addressed. Among the HOL theorem proving systems evaluated are Isabelle/HOL, Isabelle/Isar, and Coq.
Author(s): Ricky Butler (auth.), Victor A. Carreño, César A. Muñoz, Sofiène Tahar (eds.)
Series: Lecture Notes in Computer Science 2410
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2002
Language: English
Pages: 347
Tags: Software Engineering; Logic Design
Formal Methods at NASA Langley....Pages 1-2
Higher Order Unification 30 Years Later....Pages 3-12
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction....Pages 13-30
Efficient Reasoning about Executable Specifications in Coq....Pages 31-46
Verified Bytecode Model Checkers....Pages 47-66
The 5 Colour Theorem in Isabelle/Isar....Pages 67-82
Type-Theoretic Functional Semantics....Pages 83-97
A Proposal for a Formal OCL Semantics in Isabelle/HOL....Pages 99-114
Explicit Universes for the Calculus of Constructions....Pages 115-130
Formalised Cut Admissibility for Display Logic....Pages 131-147
Formalizing the Trading Theorem for the Classification of Surfaces....Pages 148-163
Free-Style Theorem Proving....Pages 164-181
A Comparison of Two Proof Critics: Power vs. Robustness....Pages 182-197
Two-Level Meta-reasoning in Coq....Pages 198-213
PuzzleTool: An Example of Programming Computation and Deduction....Pages 214-229
A Formal Approach to Probabilistic Termination....Pages 230-245
Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm....Pages 246-262
Quotient Types: A Modular Approach....Pages 263-280
Sequent Schema for Derived Rules....Pages 281-297
Algebraic Structures and Dependent Records....Pages 298-313
Proving the Equivalence of Microstep and Macrostep Semantics....Pages 314-331
Weakest Precondition for General Recursive Programs Formalized in Coq....Pages 332-347
