Overview

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.

Full Product Details

Author:   Victor A. Carreno ,  Cesar A. Munoz ,  Sofiene Tahar
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Edition:   2002 ed.
Volume:   2410
Dimensions:   Width: 15.50cm , Height: 1.90cm , Length: 23.50cm
Weight:   1.130kg
ISBN:  

9783540440390

ISBN 10:   3540440399
Pages:   347
Publication Date:   07 August 2002
Audience:   College/higher education ,  Professional and scholarly ,  Undergraduate ,  Postgraduate, Research & Scholarly
Format:   Paperback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of Contents

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.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions