Amazon cover image
Image from Amazon.com

Theorem proving in higher order logics : 14th international conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001 : proceedings / Richard J. Boulton, Paul B. Jackson (eds.).

By: Contributor(s): Material type: TextTextSeries: Lecture notes in computer science ; 2152.Publication details: Berlin ; New York : Springer, ©2001.Description: 1 online resource (x, 393 pages) : illustrationsContent type:
  • text
Media type:
  • computer
Carrier type:
  • online resource
ISBN:
  • 9783540447559
  • 3540447555
Subject(s): Genre/Form: Additional physical formats: Print version:: Theorem proving in higher order logics.DDC classification:
  • 004/.01/51 21
LOC classification:
  • QA76.9.A96 T655 2001
Online resources:
Contents:
Invited Talks -- JavaCard Program Verification -- View from the Fringe of the Fringe -- Using Decision Procedures with a Higher-Order Logic -- Regular Contributions -- Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS -- An Irrational Construction of? from? -- HELM and the Semantic Math-Web -- Calculational Reasoning Revisited An Isabelle/Isar Experience -- Mechanical Proofs about a Non-repudiation Protocol -- Proving Hybrid Protocols Correct -- Nested General Recursion and Partiality in Type Theory -- A Higher-Order Calculus for Categories -- Certifying the Fast Fourier Transform with Coq -- A Generic Library for Floating-Point Numbers and Its Application to Exact Computing -- Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain -- Abstraction and Refinement in Higher Order Logic -- A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL -- Representing Hierarchical Automata in Interactive Theorem Provers -- Refinement Calculus for Logic Programming in Isabelle/HOL -- Predicate Subtyping with Predicate Sets -- A Structural Embedding of Ocsid in PVS -- A Certified Polynomial-Based Decision Procedure for Propositional Logic -- Finite Set Theory in ACL2 -- The HOL/NuPRL Proof Translator -- Formalizing Convex Hull Algorithms -- Experiments with Finite Tree Automata in Coq -- Mizar Light for HOL Light.
Summary: This book constitutes the thoroughly refereed proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001, held in Edinburgh, Scotlang, UK in September 2001. The 23 revised full papers presented together with one invited paper and two invited abstracts were carefully reviewed and selected from a total of 47 submissions. All current issues in HOL theorem proving and formal verification of hardware and software systems are addressed. Among the HOL theorem proving systems evaluated are Coq, HOL, Isabelle, and PVS.
Holdings
Item type Current library Collection Call number Status Date due Barcode Item holds
eBook eBook e-Library eBook LNCS Available
Total holds: 0

Includes bibliographical references and index.

This book constitutes the thoroughly refereed proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001, held in Edinburgh, Scotlang, UK in September 2001. The 23 revised full papers presented together with one invited paper and two invited abstracts were carefully reviewed and selected from a total of 47 submissions. All current issues in HOL theorem proving and formal verification of hardware and software systems are addressed. Among the HOL theorem proving systems evaluated are Coq, HOL, Isabelle, and PVS.

Invited Talks -- JavaCard Program Verification -- View from the Fringe of the Fringe -- Using Decision Procedures with a Higher-Order Logic -- Regular Contributions -- Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS -- An Irrational Construction of? from? -- HELM and the Semantic Math-Web -- Calculational Reasoning Revisited An Isabelle/Isar Experience -- Mechanical Proofs about a Non-repudiation Protocol -- Proving Hybrid Protocols Correct -- Nested General Recursion and Partiality in Type Theory -- A Higher-Order Calculus for Categories -- Certifying the Fast Fourier Transform with Coq -- A Generic Library for Floating-Point Numbers and Its Application to Exact Computing -- Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain -- Abstraction and Refinement in Higher Order Logic -- A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL -- Representing Hierarchical Automata in Interactive Theorem Provers -- Refinement Calculus for Logic Programming in Isabelle/HOL -- Predicate Subtyping with Predicate Sets -- A Structural Embedding of Ocsid in PVS -- A Certified Polynomial-Based Decision Procedure for Propositional Logic -- Finite Set Theory in ACL2 -- The HOL/NuPRL Proof Translator -- Formalizing Convex Hull Algorithms -- Experiments with Finite Tree Automata in Coq -- Mizar Light for HOL Light.

Powered by Koha