Common HOL is a standard for basic HOL system functionality promoted by Proof Technologies, with the intention of enabling portability of proofs and source code between systems. Its components are more-or-less common to every system in the HOL family of theorem provers. It consists of an API, a standard HOL theory, 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.
We have written a paper describing Common HOL.
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 fully described in the following document:
We have developed a proprietary proof exporter for HOL Light, and free proof importers for HOL Light and HOL Zero. These have been used to successfully port two out of four parts of the Flyspeck project to HOL Zero.