Girish Mahajan

HOL Light

Updated on
Share on FacebookTweet on TwitterShare on LinkedIn

HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations. HOL Light is authored and maintained by the mathematician and computer scientist John Harrison. HOL Light is released under the simplified BSD license.

Logical foundations

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).


HOL Light Wikipedia

Similar Topics
Final Analysis
Hafþór Júlíus Björnsson
Denís Milar