Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs’98 Canberra, Australia September 27–October 1, 1998 Proceedings

Tobias Nipkow (auth.), Jim Grundy, Malcolm Newey (eds.)3540649875, 9783540649878

This book constitutes the refereed proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’98, held in Canberra, Australia, in September/October 1998.
The 26 revised full papers presented were carefully reviewed and selected from a total of 52 submissions. Also included are two invited papers. The papers address all current aspects of theorem proving in higher order logics and formal verification and program analysis. Besides the HOL system, the theorem provers Coq, Isabelle, LAMBDA, LEGO, NuPrl, and PVS are discussed.

---

Table of contents :
Verified lexical analysis….Pages 1-15
Extending window inference….Pages 17-32
Program abstraction in a higher-order logic framework….Pages 33-48
The village telephone system: A case study in formal software engineering….Pages 49-66
Generating embeddings from denotational descriptions….Pages 67-86
An interface between CLAM and HOL….Pages 87-104
Classical propositional decidability via Nuprl proof extraction….Pages 105-122
A comparison of PVS and Isabelle/HOL….Pages 123-142
Adding external decision procedures to HOL90 securely….Pages 143-152
Formalizing basic first order model theory….Pages 153-170
Formalizing Dijkstra….Pages 171-188
Mechanical verification of total correctness through diversion verification conditions….Pages 189-206
A type annotation scheme for Nuprl….Pages 207-224
Verifying a garbage collection algorithm….Pages 225-244
Hot: A concurrent automated theorem prover based on higher-order tableaux….Pages 245-261
Free variables and subexpressions in higher-order meta logic….Pages 263-276
An LPO-based termination ordering for higher-order terms without λ-abstraction….Pages 277-293
Proving isomorphism of first-order logic proof systems in HOL….Pages 295-314
Exploiting parallelism in interactive theorem provers….Pages 315-330
I/O automata and beyond: Temporal logic and abstraction in Isabelle….Pages 331-348
Object-oriented verification based on record subtyping in Higher-Order Logic….Pages 349-366
On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system….Pages 367-386
Co-inductive axiomatization of a synchronous language….Pages 387-399
Formal specification and theorem proving breakthroughs in geometric modeling….Pages 401-422
A tool for data refinement….Pages 423-441
Mechanizing relevant logics with HOL….Pages 443-460
Case studies in meta-level theorem proving….Pages 461-478
Formalization of graph search algorithms and its applications….Pages 479-496