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.