Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Higher Order Logic Theorem Proving and Its Applications

8th International Workshop, Aspen Grove, UT, USA, September 11 - 14, 1995. Proceedings

  • Conference proceedings
  • © 1995

Overview

Editors:
  1. E. Thomas Schubert
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Philip J. Windley
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. James Alves-Foss
    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 971)

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 USD 54.99
Price excludes VAT (USA)
  • 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

Table of contents (26 papers)

  1. Front Matter

    Download chapter PDF

  2. Mechanizing a π-calculus equivalence in HOL

    • Otmane Aït Mohamed
    Pages 1-16

  3. Non-primitive recursive function definitions

    • Sten Agerholm
    Pages 17-31

  4. Experiments with ZF set theory in HOL and Isabelle

    • Sten Agerholm, Mike Gordon
    Pages 32-45

  5. Automatically synthesized term denotation predicates: A proof aid

    • Paul E. Black, Phillip J. Windley
    Pages 46-57

  6. On the refinement of symmetric memory protocols

    • J. -P. Bodeveix, M. Filali
    Pages 58-74

  7. Combining decision procedures in the HOL system

    • Richard J. Boulton
    Pages 75-89

  8. Deciding cryptographic protocol adequacy with HOL

    • Stephen H. Brackin
    Pages 90-105

  9. A practical method for reasoning about distributed systems in a theorem prover

    • Holger Busch
    Pages 106-121

  10. A theory of finite maps

    • Graham Collins, Donald Syme
    Pages 122-137

  11. Virtual theories

    • Paul Curzon
    Pages 138-153

  12. An automata theory dedicated towards formal circuit synthesis

    • Dirk Eisenbiegler, Ramayya Kumar
    Pages 154-169

  13. Interfacing HOL90 with a functional database query language

    • Elsa L. Gunter, Leonid Libkin
    Pages 170-185

  14. Floating point verification in HOL

    • John Harrison
    Pages 186-199

  15. Inductive definitions: Automation and application

    • John Harrison
    Pages 200-213

  16. A formulation of TLA in Isabelle

    • Sara Kalvala
    Pages 214-228

  17. Formal verification of serial pipeline multipliers

    • Jang Dae Kim, Shiu-Kai Chin
    Pages 229-244

  18. TkWinHOL: A tool for Window Inference in HOL

    • Thomas LÃ¥ngbacka, Rimvydas RukÅ¡Ä—nas, Joakim von Wright
    Pages 245-260

  19. Formal verification of counterflow pipeline architecture

    • Paul N. Loewenstein
    Pages 261-276

  20. Deep embedding VHDL

    • Ralf Reetz
    Pages 277-292
Back to top

Keywords

About this book

This book constitutes the proceedings of the 8th International Conference on Higher Order Logic Theorem Proving and Its Applications, held in Aspen Grove, Utah, USA in September 1995.
The 26 papers selected by the program committee for inclusion in this volume document the advances in the field achieved since the predecessor conference. The papers presented fall into three general categories: representation of formalisms in higher order logic; applications of mechanized higher order logic; and enhancements to the HOL and other theorem proving systems.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation