Common HOL

The Common HOL Project

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.

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