HOL4
Kananaskis 10
[HOL logo]
Easier to use: easy installation, bugs fixed!
Cool examples: ARMv7, λ-calculus, ACL2, Verified Lisp
New libraries: SMT tool integration, fixed-width integers (words)
New documentation: Extended Description, DPLL example, ...
[Picture of Lake Kananaskis taken by Alan Kane (akane@cadvision.com)]
Release notes |  Documentation |  FAQ |  Online reference |  Emacs mode |  Installing from Sources  |  Windows installer |  HOL@github |  Anon Git |  HOLω |
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 and BDD engines. HOL4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.

Other HOLs are described elsewhere.

Downloads
History
During the last 20 years there have been several widely used versions of the HOL system:
  1. HOL88 from Cambridge;
  2. HOL90 from Calgary and Bell Labs;
  3. HOL98 from Cambridge, Glasgow and Utah.
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 HOL Light. 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.
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:

Acknowledgments

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).

[SourceForge Logo]

Time-stamp: "Monday, 10 November 2014; 05:42 UTC (Michael Norrish)"