TY  - BOOK
AU  - Carreño,Victor A.
AU  - Muñoz,César A.
AU  - Tahar,Sofiène
ED  - SpringerLink (Online service)
TI  - Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002 Hampton, VA, USA, August 20–23, 2002 Proceedings 
T2  - Lecture Notes in Computer Science,
SN  - 9783540456858
AV  - QA76.758 
U1  - 005.1 23
PY  - 2002///
CY  - Berlin, Heidelberg
PB  - Springer Berlin Heidelberg
KW  - Computer science
KW  - Logic design
KW  - Software engineering
KW  - Computer Science
KW  - Software Engineering
KW  - Logic Design
N1  - 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
UR  - http://dx.doi.org/10.1007/3-540-45685-6
ER  -