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.


Tom Melham
Department of Computing Science
Glasgow University
G12 8QQ

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:

Related Documents:

There is an extensive online HOL bibliography.