+612 9045 4394
Theorem Proving in Higher Order Logics : 10th International Conference, Tphols'97, Murray Hill, Nj, Usa, August 19-22, 1997, Proceedings - Elsa L. Gunter

Theorem Proving in Higher Order Logics

10th International Conference, Tphols'97, Murray Hill, Nj, Usa, August 19-22, 1997, Proceedings

By: Elsa L. Gunter (Editor), Amy Felty (Editor)

Paperback Published: 6th August 1997
ISBN: 9783540633792
Number Of Pages: 346

Share This Book:


or 4 easy payments of $33.88 with Learn more
Ships in 7 to 10 business days

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.

An Isabelle-Based Theorem Prover for VDM-SLp. 1
Executing Formal Specifications by Translation to Higher Order Logic Programmingp. 17
Human-Style Theorem Proving Using PVSp. 33
A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processorp. 49
Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysisp. 69
ML Programming in Constructive Type Theoryp. 87
Possibly infinite Sequences in Theorem Provers: A Comparative Studyp. 89
Proof Normalization for a First-Order Formulation of Higher-Order Logicp. 105
Using a PVS Embedding of CSP to Verify Authentication Protocolsp. 121
Verifying the Accuracy of Polynomial Approximations in HOLp. 137
A Full Formalisation of [pi]-Calculus Theory in the Calculus of Constructionsp. 153
Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verificationp. 171
Refining Reactive Systems in HOL Using Action Systemsp. 183
On Formalization of Bicategory Theoryp. 199
Towards an Object-Oriented Progification Languagep. 215
Verification for Robust Specificationp. 231
A Theory of Structured Model-Based Specifications in Isabelle/HOLp. 243
Proof Presentation for Isabellep. 259
Derivation and Use of Induction Schemes in Higher-Order Logicp. 275
Higher Order Quotients and their Implementation in Isabelle HOLp. 291
Type Classes and Overloading in Higher-Order Logicp. 307
A Comparative Study of Coq and HOLp. 323
Author Indexp. 339
Table of Contents provided by Blackwell. All Rights Reserved.

ISBN: 9783540633792
ISBN-10: 3540633790
Series: Studies in Economic Ethics and Philosophy : Book Vol. 127
Audience: General
Format: Paperback
Language: English
Number Of Pages: 346
Published: 6th August 1997
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 1.88
Weight (kg): 0.5