HOL 4 Kananaskis 4  
HOL logo
Easier to use: easy installation, bugs fixed!
Cool examples: ARM6, λ-calculus, PSL, ACL2
New libraries: BDDs, SAT, model-checking
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@S/F |  Anon SVN | 

 

What is HOL 4?
It is the latest version of the HOL automated proof system 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. An oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.
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.
HOL 4 is the successor to these. Its development was partly supported by the PROSPER project. HOL 4 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
SourceForge Logo HOL 4 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:

Time-stamp: "Monday, 7 January 2008; 04:57 UTC (Michael Norrish)"