Skip to main content
SpringerLink
Log in
Book cover
  • Conference proceedings
  • © 1995

Higher Order Logic Theorem Proving and Its Applications

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

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)

Sections

Buy it now

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

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

Table of contents (26 papers)

  1. Front Matter

    PDF

  2. Mechanizing a π-calculus equivalence in HOL

    • Otmane Aït Mohamed
    Pages 1-16

  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

  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

  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

  20. Deep embedding VHDL

    • Ralf Reetz
    Pages 277-292
Back to top

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.
Back to top

Keywords

Back to top

Bibliographic Information

Back to top

Publish with us

Policies and ethics

Back to top
Access via your institution

Buy it now

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

Search

Navigation