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.Mike Gordon has also written a useful history of HOL.
Introduction to HOL: A theorem proving environment for higher order logic
(Cambridge University Press, 1993).
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.
T. Melham, ‘ Automating Recursive Type Definitions in Higher Order Logic’,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:
in Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 341-386.
T. Melham, ‘A Package for Inductive Relation Definitions in HOL’,Juanito Camilleri and I subsequently wrote a longer technical report on making formal inductive definitions in higher order logic, with examples:
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.
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.