Common HOL is a standard for basic HOL system functionality that is more-or-less common to every system in the HOL family of theorem provers, aimed at facilitating portability of source code and proofs between HOL systems. It consists of an API, adapted versions of various HOL systems to support the API, a proof object file format, and a proof object importer and exporter for various HOL systems.
The API has around 430 components, including approximately:
The API is documented as part of the HOL Zero system.
The API has been implemented for HOL Light and HOL Zero, and is free. Please contact us if interested in obtaining these.
The proof object file format is a semi-human-readable textual format designed for flexibility and fast lexical analysis. It allows a mixture of Hilbert-style step sequences and steps with parenthesised substeps. It is documented here.
We have developed a proprietary proof exporter for HOL Light, and free proof importers for HOL Light and HOL Zero. Please contact us if interested in obtaining these.