دانلود کتاب Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002 Hampton, VA, USA, August 20–23, 2002 Proceedings

فهرست مطالب :

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