**constructive mathematics**, **realizability**, **computability**

propositions as types, proofs as programs, computational trinitarianism

*HOL Light* is a proof assistant which is a variant of the *HOL* system.

The Kepler conjecture was formalized and proven using *HOL Light* (in the *Flyspeck project*).

- John Harrison,
*The HOL Light theorem prover*

Created on November 1, 2014 at 16:52:09. See the history of this page for a list of all contributions to it.