About

What is HOL?

The HOL interactive theorem prover is a 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. HOL is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.

Other HOLs are described elsewhere.

HOL is free software, released under the Modified (3-clause) BSD licence.

Who uses HOL?

Notable projects using HOL include:

CakeML, a functional programming language with an ecosystem of proofs and tools, including a self-bootstrapping, proven-correct compiler.
HOL4P4, a small-step, heapless formalisation and a type system of the P4 language.
HolBA, a library that provides tools for analysis and formal proofs of properties of programs in binary format that use the ARMv8, RISC-V and Cortex-M0 instruction sets.
Verifereum, an open-source project that brings mathematical rigour to Ethereum smart contract verification.

This is a partial list of projects utilizing HOL. Many other research and industry applications exist.

Join our community! Whether you're an experienced HOL4 developer or new to formal verification, we welcome your contributions. Learn more in our Community section to find out how to join the mailing lists, chat rooms, and contribute to HOL-based projects.

History

Participants of the first HOL users meeting — 1st HOL Users Meeting in Cambridge, 1988, at Sidney Sussex college1^,2

During the last 30 years there have been several widely used versions of the HOL system:

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

The logo is a reference to a photo of a snow-viewing lantern in the late Mike Gordon's garden, which appeared on the cover of the HOL88 system documentation.3

The current version, and successor to those above, is HOL4. Its development was partly supported by the PROSPER project. HOL4 is based on HOL98 and incorporates ideas and tools from HOL Light.

To learn more about the history of HOL, consider reading Mike Gordon's paper 'From LCF to HOL: a short history' (2000), or Anthony Fox's slides on Specifications and theorem-proving @ Arm (Opening of the Workshop for HOL4 users 2024).

Acknowledgments

HOL is developed by people at (among other places):

We would also like to acknowledge the support of Zulip (for sponsored hosting of our chat), Sourceforge (for some file downloads in the past and mailing lists), and GitHub (for our code repository and issue tracker).

1 Identified participants with affiliations at the time (left to right):
Back: Juanito Camilleri (Cambridge), Roger Hale (Cambridge), Jeff Joyce (Cambridge), Albert Camilleri (Cambridge), Thomas Forster (Cambridge), Andy Pitts (Cambridge), Rachel Cardell-Oliver (Cambridge), ?, ?
Middle: ?, Ton Kalker (Philips Eindhoven), Konrad Slind (Calgary), Kevin Blackburn (ICL), Roger Jones (ICL), Paul Curzon (Cambridge), ?, ?, Phil Windley (Idaho), ?
Front: Tom Melham (Cambridge), ?, Paul Loewenstein (Sun), Mike Gordon (Cambridge), Avra Cohn (Cambridge), Robin Milner (Cambridge), Larry Paulson (Cambridge), Inder Dhingra (Cambridge), Shiu-Kai Chin (Syracuse), Elsa Gunter (U. Penn)

2 History of early HOL meetings, including more photographs

3 Source: Michael J. C. Gordon - Snow watching lantern