10. TPHOLs 1997: Murray Hill, NJ, USA

Elsa L. Gunter, Amy P. Felty (Eds.): Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings. Lecture Notes in Computer Science 1275 Springer 1997, ISBN 3-540-63379-0

Sten Agerholm, Jacob Frost:
An Isabelle-Based Theorem Prover for VDM-SL. 1-16
James H. Andrews:
Executing Formal Specifications by Translation to Higher Order Logic Programming. 17-32
Myla Archer, Constance L. Heitmeyer:
Human-Style Theorem Proving Using PVS. 33-48
Albert John Camilleri:
A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processor. 49-67
Boutheina Chetali, Barbara Heyd:
Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis. 69-85
Robert L. Constable:
ML Programming in Constructive Type Theory (abstract). 87
Marco Devillers, W. O. David Griffioen, Olaf Müller:
Possibly Infinite Sequences in Theorem Provers: A Comparative Study. 89-104
Gilles Dowek:
Proof Normalization for a First-Order Formulation of Higher-Order Logic. 105-119
Bruno Dutertre, Steve Schneider:
Using a PVS Embedding of CSP to Verify Authentication Protocols. 121-136
John Harrison:
Verifying the Accuracy of Polynomial Approximations in HOL. 137-152
Daniel Hirschkoff:
A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions. 153-169
Deepak Kapur:
Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification. 171-182
Thomas Långbacka, Joakim von Wright:
Refining Reactive Systems in HOL Using Action Systems. 183-197
Takahisa Mohri:
On Formalization of Bicategory Theory. 199-214
Wolfgang Naraschewski:
Towards an Object-Oriented Progification Language. 215-230
Doron Peled:
Verification for Robust Specification. 231-241
Thomas Santen:
A Theory of Structured Model-Based Specifications in Isabelle/HOL. 243-258
Martin Simons:
Proof Presentation for Isabelle. 259-274
Konrad Slind:
Derivation and Use of Induction Schemes in Higher-Order Logic. 275-290
Oscar Slotosch:
Higher Order Quotients and their Implementation in Isabelle HOL. 291-306
Markus Wenzel:
Type Classes and Overloading in Higher-Order Logic. 307-322
Vincent Zammit:
A Comparative Study of Coq and HOL. 323-337

Last update Fri May 25 08:43:21 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page