HOL Light is a proof assistant for classical higher-order logic.
HOL Light is authored and maintained by the mathematician and computer scientist John Harrison.
HOL Light is released under the simplified BSD license.
[1] HOL Light is based on a formulation of type theory with equality as the only primitive notion.
The primitive rules of inference are the following: This formulation of type theory is very close to the one described in section II.2 of Lambek & Scott (1986).