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

Common HOL

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.

HOL Glossary

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.