Cover Image
Read Now

Theorem Proving in Higher Order Logics 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001. Proceedings

This volume constitutes the proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001) held 3–6 September 2001 in Edinburgh, Scotland. TPHOLs covers all aspects of theorem proving in higher order logics, as well as related topics in theorem proving and v...

Full description

Bibliographic Details
Other Authors: Boulton, Richard J. (Editor), Jackson, Paul B. (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 2001, 2001
Edition:1st ed. 2001
Series:Lecture Notes in Computer Science
Subjects:
Compilers (computer Programs)
Computer Science Logic And Foundations Of Programming
Compilers And Interpreters
Software Engineering
Computer Science
Artificial Intelligence
Formal Languages And Automata Theory
Machine Theory
Theory Of Computation
Online Access:
Collection: Springer Book Archives -2004 - Collection details see MPG.ReNa
Table of 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

Similar Items