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.

Minmalist OCaml

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.