Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs 97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings - researchr publication

researchr

You are not signed in
Sign in
Sign up

Elsa L. Gunter, Amy P. Felty, editors, Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs 97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings. Volume 1275 of Lecture Notes in Computer Science, Springer, 1997.

Conference: tphol1997

Abstract is missing.

An Isabelle-Based Theorem Prover for VDM-SLSten Agerholm, Jacob Frost. 1-16

Executing Formal Specifications by Translation to Higher Order Logic ProgrammingJames H. Andrews. 17-32

Human-Style Theorem Proving Using PVSMyla Archer, Constance L. Heitmeyer. 33-48

A Hybrid Approach to Verifying Liveness in a Symmetric Multi-ProcessorAlbert John Camilleri. 49-67

Formal Verification of Concurrent Programs in LP and in COQ: A Comparative AnalysisBoutheina Chetali, Barbara Heyd. 69-85

ML Programming in Constructive Type Theory (abstract)Robert L. Constable. 87

Possibly Infinite Sequences in Theorem Provers: A Comparative StudyMarco Devillers, W. O. David Griffioen, Olaf Müller. 89-104

Proof Normalization for a First-Order Formulation of Higher-Order LogicGilles Dowek. 105-119

Using a PVS Embedding of CSP to Verify Authentication ProtocolsBruno Dutertre, Steve Schneider. 121-136

Verifying the Accuracy of Polynomial Approximations in HOLJohn Harrison. 137-152

A Full Formalisation of pi-Calculus Theory in the Calculus of ConstructionsDaniel Hirschkoff. 153-169

Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware VerificationDeepak Kapur. 171-182

Refining Reactive Systems in HOL Using Action SystemsThomas Långbacka, Joakim von Wright. 183-197

On Formalization of Bicategory TheoryTakahisa Mohri. 199-214

Towards an Object-Oriented Progification LanguageWolfgang Naraschewski. 215-230

Verification for Robust SpecificationDoron Peled. 231-241

A Theory of Structured Model-Based Specifications in Isabelle/HOLThomas Santen. 243-258

Proof Presentation for IsabelleMartin Simons. 259-274

Derivation and Use of Induction Schemes in Higher-Order LogicKonrad Slind. 275-290

Higher Order Quotients and their Implementation in Isabelle HOLOscar Slotosch. 291-306

Type Classes and Overloading in Higher-Order LogicMarkus Wenzel. 307-322

A Comparative Study of Coq and HOLVincent Zammit. 323-337

runs on WebDSL