This book constitutes the refereed proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '97, held in Murray Hill, NJ, USA, in August 1997.
The volume presents 19 carefully revised full papers selected from 32 submissions during a thorough reviewing process. The papers cover work related to all aspects of theorem proving in higher order logics, particularly based on secure mechanization of those logics; the theorem proving systems addressed include Coq, HOL, Isabelle, LEGO, and PVS.
Author(s): Sten Agerholm, Jacob Frost (auth.), Elsa L. Gunter, Amy Felty (eds.)
Series: Lecture Notes in Computer Science 1275
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1997
Language: English
Pages: 346
Tags: Mathematical Logic and Formal Languages; Logic Design; Software Engineering; Logics and Meanings of Programs; Mathematical Logic and Foundations
An Isabelle-based theorem prover for VDM-SL....Pages 1-16
Executing formal specifications by translation to higher order logic programming....Pages 17-32
Human-style theorem proving using PVS....Pages 33-48
A hybrid approach to verifying liveness in a symmetric multi-processor....Pages 49-67
Formal verification of concurrent programs in L p and in C oq : A comparative analysis....Pages 69-85
ML programming in constructive type theory....Pages 87-87
Possibly infinite sequences in theorem provers: A comparative study....Pages 89-104
Proof normalization for a first-order formulation of higher-order logic....Pages 105-119
Using a PVS embedding of CSP to verify authentication protocols....Pages 121-136
Verifying the accuracy of polynomial approximations in HOL....Pages 137-152
A full formalisation of π-calculus theory in the calculus of constructions....Pages 153-169
Rewriting, decision procedures and lemma speculation for automated hardware verification....Pages 171-182
Refining reactive systems in HOL using action systems....Pages 183-197
On formalization of bicategory theory....Pages 199-214
Towards an object-oriented progification language....Pages 215-230
Verification for robust specification....Pages 231-241
A theory of structured model-based specifications in Isabelle/HOL....Pages 243-258
Proof presentation for Isabelle....Pages 259-274
Derivation and use of induction schemes in higher-order logic....Pages 275-290
Higher order quotients and their implementation in Isabelle HOL....Pages 291-306
Type classes and overloading in higher-order logic....Pages 307-322
A comparative study of Coq and HOL....Pages 323-337
