Proof Technologies Ltd
Home | Software | Publications | Various | Contact Us

Common HOL

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.

Common HOL API

The API has around 430 components, including approximately:

  • 100 functional programming library utilities
  • 35 HOL type, term and theorem utilities
  • 125 HOL syntax functions
  • 30 HOL theory commands
  • 85 HOL inference rules
  • 40 HOL theorems
  • 15 HOL fixity, parsing and printing functions

    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.

    Common HOL Proof Porting

    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:

    Download: CommonHOL_Proof_Object_Format-0.5.txt

    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.