The HOL Theorem Prover for Higher Order Logic

The HOL Theorem Prover is a general and widely-used computer program for constructing specifications and formal proofs in higher order logic. The system is used in industry and academia to support formal reasoning in many different areas, including hardware design and verification, reasoning about security, proofs about real-time systems, semantics of hardware description languages, compiler verification, program correctness, modelling concurrency, and program refinement. HOL is also used as an open platform for general theorem-proving research, and as a platform for formalized mathematics.

HOL is described in detail in the book

M. J. C. Gordon and T. F. Melham, eds.
Introduction to HOL: A theorem proving environment for higher order logic
(Cambridge University Press, 1993).
Mike Gordon wrote a useful history of HOL.

The HOL SourceForge website provides information and documentation on the current release of HOL, and you can also download the system from this website. For developer information, see the HOL project page on SourceForge.

Research Papers on Early HOL Tools

Two of my major, early contributions to the HOL system were a package for defining algebraic data types in HOL's higher-order object logic, and a package for making inductive predicate and relation definitions. The method for data type definitions is explained in detail in
T. Melham, ‘ Automating Recursive Type Definitions in Higher Order Logic’,
in Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 341-386.
This paper is still a useful resource for anyone wanting to learn about how types may be introduced by formal definitions, as opposed to axioms, into a higher order logic. The inductive definitions tool was first described in a paper presented at the 1991 HOL workshop:
T. Melham, ‘A Package for Inductive Relation Definitions in HOL’,
in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991, edited by M. Archer, J. J. Joyce, K. N. Levitt and P. J. Windley (IEEE Computer Society Press, 1992), pp. 350-357.
Juanito Camilleri and I subsequently wrote a longer technical report on making formal inductive definitions in higher order logic, with examples:
J. Camilleri and T. Melham, ‘Reasoning with Inductively Defined Relations in the HOL Theorem Prover’, Technical Report 265, Computer Laboratory, University of Cambridge (August 1992).
Readers may find this a useful tutorial introduction to the subject of inductively defined predicates and relations.
Tom Melham, last updated in September 2005.