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 and BDD engines. HOL4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.

Other HOLs are described elsewhere.

• Sources (and also, via git)
• Windows installer

1. HOL88 from Cambridge;
2. HOL90 from Calgary and Bell Labs;
3. HOL98 from Cambridge, Glasgow and Utah.

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)
  • [hol-info@lists.sourceforge.net | subscribe | Gmane Archives | S/F archives ]
• the #hol IRC channel on freenode provides a real-time counterpart to the mailing list
• Bug reports: 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).