Skip to main content
SpringerLink
Log in
Book cover

Theorem Proving in Higher Order Logics

9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings

  • Conference proceedings
  • © 1996

Overview

Editors:
  1. Gerhard Goos
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Juris Hartmanis
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Jan Leeuwen
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  4. Joakim Wright
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  5. Jim Grundy
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  6. John Harrison
    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 1125)

Included in the following conference series:

Conference proceedings info: TPHOLs 1996.

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

Access this book

Log in via an institution

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (28 papers)

  1. Front Matter

    Download chapter PDF

  2. Translating specifications in VDM-SL to PVS

    • Sten Agerholm
    Pages 1-16

  3. A comparison of HOL and ALF formalizations of a categorical coherence theorem

    • Sten Agerholm, Ilya Beylin, Peter Dybjer
    Pages 17-32

  4. Modeling a hardware synthesis methodology in isabelle

    • David Basin, Stefan Friedrich
    Pages 33-50

  5. Inference rules for programming languages with side effects in expressions

    • Paul E. Black, Phillip J. Windley
    Pages 51-60

  6. Deciding cryptographic protocol adequacy with HOL: The implementation

    • Stephen H. Brackin
    Pages 61-76

  7. Proving liveness of fair transition systems

    • Holger Busch
    Pages 77-92

  8. Program derivation using the refinement calculator

    • Michael Butler, Thomas Långbacka
    Pages 93-108

  9. A proof tool for reasoning about functional programs

    • Graham Collins
    Pages 109-124

  10. Coq and hardware verification: A case study

    • Solange Coupet-Grimal, Line Jakubiec
    Pages 125-139

  11. Elements of mathematical analysis in PVS

    • Bruno Dutertre
    Pages 141-156

  12. Implementation issues about the embedding of existing high level synthesis algorithms in HOL

    • Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar
    Pages 157-172

  13. Five axioms of alpha-conversion

    • Andrew D. Gordon, Tom Melham
    Pages 173-190

  14. Set theory, higher order logic or both?

    • Mike Gordon
    Pages 191-201

  15. A mizar mode for HOL

    • John Harrison
    Pages 203-220

  16. Stålmarck’s algorithm as a HOL derived rule

    • John Harrison
    Pages 221-234

  17. Towards applying the composition principle to verify a microkernel operating system

    • Mark R. Heckman, Cui Zhang, Brian R. Becker, Dave Peticolas, Karl N. Levitt, Ron A. Olsson
    Pages 235-250

  18. A modular coding of UNITY in COQ

    • Barbara Heyd, Pierre Crégut
    Pages 251-266

  19. Importing mathematics from HOL into Nuprl

    • Douglas J. Howe
    Pages 267-281

  20. A structure preserving encoding of Z in isabelle/HOL

    • Kolyang, T. Santen, B. Wolff
    Pages 283-298
Back to top

Other volumes

  1. Theorem Proving in Higher Order Logics

Keywords

About this book

This book constitutes the refereed proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996.
The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an up-to-date report on the state of the art in this increasingly active field.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation