Skip to main content
SpringerLink
Log in

Higher Order Logic Theorem Proving and Its Applications

7th International Workshop, Valletta, Malta, September 19-22, 1994. Proceedings

  • Conference proceedings
  • © 1994

Overview

Editors:
  1. Thomas F. Melham
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Juanito Camilleri
    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 859)

Included in the following conference series:

Conference proceedings info: HUG 1994.

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 (30 papers)

  1. Front Matter

    Download chapter PDF

  2. LCF examples in HOL

    • Sten Agerholm
    Pages 1-16

  3. A graphical tool for proving UNITY progress

    • Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson
    Pages 17-32

  4. Reasoning about a class of linear systems of equations in HOL

    • Catia M. Angelo, Luc Claesen, Hugo De Man
    Pages 33-48

  5. Towards a HOL theory of memory

    • J. -P. Bodeveix, M. Filali, P. Roche
    Pages 49-64

  6. Providing tractable security analyses in HOL

    • Stephen H. Brackin
    Pages 65-80

  7. Highlighting the lambda-free fragment of Automath

    • N. G. de Bruijn
    Pages 81-96

  8. First-order automation for higher-order-logic theorem proving

    • Holger Busch
    Pages 97-112

  9. Symbolic animation as a proof tool

    • Juanito Camilleri, Vincent Zammit
    Pages 113-127

  10. Datatypes in L2

    • Nick Chapman, Simon Finn, Michael P. Fourman
    Pages 128-143

  11. A formal theory of undirected graphs in higher-order logc

    • Ching-Tsun Chou
    Pages 144-157

  12. Mechanical verification of distributed algorithms in higher-order logic

    • Ching-Tsun Chou
    Pages 158-176

  13. Tracking design changes with formal verification

    • Paul Curzon
    Pages 177-192

  14. Weak systems of set theory related to HOL

    • Thomas Forster
    Pages 193-204

  15. Interval-semantic component models and the efficient verification of transaction-level circuit behavior

    • David A. Fura, Arun K. Somani
    Pages 205-220

  16. An interpretation of Noden in HOL

    • Brian T. Graham
    Pages 221-234

  17. Reasoning about real circuits

    • Keith Hanna
    Pages 235-253

  18. Binary decision diagrams as a HOL derived rule

    • John Harrison
    Pages 254-268

  19. Trustworthy tools for trustworthy programs: A verified verification condition generator

    • Peter V. Homeier, David F. Martin
    Pages 269-284

  20. S: A machine readable specification notation based on higher order logic

    • J. Joyce, N. Day, M. Donat
    Pages 285-299
Back to top

Other volumes

  1. Higher Order Logic Theorem Proving and Its Applications

Keywords

About this book

This volume presents the proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications held in Valetta, Malta in September 1994.
Besides 3 invited papers, the proceedings contains 27 refereed papers selected from 42 submissions. In total the book presents many new results by leading researchers working on the design and applications of theorem provers for higher order logic. In particular, this book gives a thorough state-of-the-art report on applications of the HOL system, one of the most widely used theorem provers for higher order logic.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation