Theorem Proving in Higher Order Logics

15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings

364 Seiten, Taschenbuch

Kurzbeschreibung des Verlags

Invited Talks.- Formal Methods at NASA Langley.- Higher Order Unification 30 Years Later.- Regular Papers.- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.- Efficient Reasoning about Executable Specifications in Coq.- Verified Bytecode Model Checkers.- The 5 Colour Theorem in Isabelle/Isar.- Type-Theoretic Functional Semantics.- A Proposal for a Formal OCL Semantics in Isabelle/HOL.- Explicit Universes for the Calculus of Constructions.- Formalised Cut Admissibility for Display Logic.- Formalizing the Trading Theorem for the Classification of Surfaces.- Free-Style Theorem Proving.- A Comparison of Two Proof Critics: Power vs. Robustness.- Two-Level Meta-reasoning in Coq.- PuzzleTool: An Example of Programming Computation and Deduction.- A Formal Approach to Probabilistic Termination.- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm.- Quotient Types: A Modular Approach.- Sequent Schema for Derived Rules.- Algebraic Structures and Dependent Records.- Proving the Equivalence of Microstep and Macrostep Semantics.- Weakest Precondition for General Recursive Programs Formalized in Coq.

• Reihe: Lecture Notes in Computer Science
• Themen: Informatik und Informationstechnologie Informatik Theoretische Informatik
• ISBN: 9783540440390
• Sprache: Englisch
• Erscheinungsdatum: 07.08.2002
• Größe: 235 x 155 mm
• Verlag: Springer
• Herausgegeben von: Sofiene Tahar, Cesar A. Munoz, Victor A. Carreno