default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID10th TPHOLs 1997: Murray Hill, NJ, USA
- Elsa L. Gunter, Amy P. Felty:
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 A. 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 A. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-19 22:21 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
