The HOL Theorem Prover
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
There are two versions of the system, HOL88 and HOL90.
For more details on HOL, consult the
HOL Web Page.
Department of Computing Science
Voice: (+44) 141-330-4967
FAX: (+44) 141-330-4913
Number of Users and Sites:
There is an large, active HOL communty.
The HOL88 version is the original
Cambridge HOL system built using Lisp; HOL90 is a reimplementation in Standard ML.
Both systems are freely available by ftp:
There is an extensive online