# 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.*