- What is HOL4?
HOL4 is the latest version of the HOL interactive proof
assistant for higher order logic: a programming environment in which
theorems can be proved and proof tools implemented. Built-in decision
procedures and theorem provers can automatically establish many simple
theorems (users may have to prove the hard theorems themselves!) An
oracle mechanism gives access to external programs such as SMT
engines. HOL4 is particularly suitable as a platform for implementing
combinations of deduction, execution and property checking.
Other HOLs are described elsewhere.
During the last 20 years there have been several
widely used versions of the HOL system:
HOL4 is the successor to these. Its development was partly supported by the PROSPER project.
HOL4 is based on HOL98 and incorporates ideas and tools from
The ProofPower system
is another implementation of HOL. It was originally developed by ICL,
but is now freely available from Lemma 1.
All the HOL systems use Robin Milner’s LCF approach.
- HOL88 from Cambridge;
- HOL90 from Calgary and Bell Labs;
- HOL98 from Cambridge, Glasgow and Utah.
- How easy is it to learn?
Starting from scratch, it takes on average about a month to become comfortable using HOL.
Many people learn the system from the free tutorial, others take courses that are offered from time to time.
- Support and licencing
HOL4 is an open source project with a BSD-style licence that
allows its free use in commercial products.
New developers are welcome.
Support and information is available online:
the hol-info mailing list is for
discussion, questions and announcements related to the HOL System (HOL4 and HOL Light discussions are both welcome)
- the #hol IRC channel on
freenode provides a real-time counterpart to the mailing list
Please use the
github issue tracker to report problems, and make feature suggestions.
HOL is developed by researchers at (among other places):
We would also like to acknowledge the support of Sourceforge (for file downloads and mailing lists), and Github (for our code repository and issue tracker).