The HOL Theorem Prover
The HOL
system is a powerful and widely used computer program for
constructing formal specifications and proofs in higher order
logic. The system is used in both industry and academia to support
formal reasoning in many different areas, including hardware design
and verification, reasoning about security, proofs about real-time
systems, semantics of hardware description languages, compiler
verification, program correctness, modelling concurrency, and program
refinement. HOL is also used as an open platform for general
theorem-proving research.
There are two versions of the system, HOL88 and HOL90.
For more details on HOL, consult the
HOL Web Page.
Contact:
Tom Melham
Department of Computing Science
Glasgow University
Glasgow
G12 8QQ
Email: tfm@dcs.gla.ac.uk
Voice: (+44) 141-330-4967
FAX: (+44) 141-330-4913
WWW:
http://www.dcs.gla.ac.uk/~tfm
Number of Users and Sites:
There is an large, active HOL communty.
Languages:
The HOL88 version is the original
Cambridge HOL system built using Lisp; HOL90 is a reimplementation in Standard ML.
Availability:
Both systems are freely available by ftp:
Related Documents:
There is an extensive online
HOL
bibliography.