Skip to main content
Springer Nature Link
Log in

Theorem Proving in Higher Order Logics

10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings

  • Conference proceedings
  • © 1997

Overview

Editors:
  1. Elsa L. Gunter
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Amy Felty
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 1275)

Included in the following conference series:

Conference proceedings info: TPHOLs 1997.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
Softcover Book EUR 52.74
Price includes VAT (France)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

About this book

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.

Keywords

Table of contents (22 papers)

  1. Front Matter

    Download chapter PDF

  2. An Isabelle-based theorem prover for VDM-SL

    • Sten Agerholm, Jacob Frost
    Pages 1-16

  3. Executing formal specifications by translation to higher order logic programming

    • James H. Andrews
    Pages 17-32

  4. Human-style theorem proving using PVS

    • Myla Archer, Constance Heitmeyer
    Pages 33-48

  5. A hybrid approach to verifying liveness in a symmetric multi-processor

    • Albert J. Camilleri
    Pages 49-67

  6. Formal verification of concurrent programs in Lp and in Coq: A comparative analysis

    • Boutheina Chetali, Barbara Heyd
    Pages 69-85

  7. ML programming in constructive type theory

    • Robert L. Constable
    Pages 87-87

  8. Possibly infinite sequences in theorem provers: A comparative study

    • Marco Devillers, David Griffioen, Olaf Müller
    Pages 89-104

  9. Proof normalization for a first-order formulation of higher-order logic

    • Gilles Dowek
    Pages 105-119

  10. Using a PVS embedding of CSP to verify authentication protocols

    • Bruno Dutertre, Steve Schneider
    Pages 121-136

  11. Verifying the accuracy of polynomial approximations in HOL

    • John Harrison
    Pages 137-152

  12. A full formalisation of π-calculus theory in the calculus of constructions

    • Daniel Hirschkoff
    Pages 153-169

  13. Rewriting, decision procedures and lemma speculation for automated hardware verification

    • Deepak Kapur
    Pages 171-182

  14. Refining reactive systems in HOL using action systems

    • Thomas LÃ¥ngbacka, Joakim von Wright
    Pages 183-197

  15. On formalization of bicategory theory

    • Takahisa Mohri
    Pages 199-214

  16. Towards an object-oriented progification language

    • Wolfgang Naraschewski
    Pages 215-230

  17. Verification for robust specification

    • Doron Peled
    Pages 231-241

  18. A theory of structured model-based specifications in Isabelle/HOL

    • Thomas Santen
    Pages 243-258

  19. Proof presentation for Isabelle

    • Martin Simons
    Pages 259-274

  20. Derivation and use of induction schemes in higher-order logic

    • Konrad Slind
    Pages 275-290
Back to top

Other volumes

  1. Theorem Proving in Higher Order Logics

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation