Common HOL is our standard for portability of proofs and source code across HOL
systems. See our Common HOL pages for
details about the standard and downloads for its open source components.
We have had considerable involvement in the Flyspeck project, to formalise
Hale's proof of the Kepler Conjecture. See our
Flyspeck pages for an overview of the project, as well as downloadable
proof modules for replaying the proof on Common HOL conformant systems.
We promote the demystification of theorem proving, and as part of this
endeavour provide our Glossary of HOL
Terminology. It explains the theorem proving, mathematical logic and
functional programming terminology needed to understand the implementation of
HOL systems and academic papers written about them.
We have produced a cut-down version of
OCaml 3.12.1 that has a smaller footprint and faster build time, but with
some features stripped out, that still works with our software.