HOL Light

HOL Light is a proof assistant for classical higher-order logic. It is a member of the HOL theorem prover family. 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.^[1]

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:

${\displaystyle {\cfrac {\qquad }{\vdash t=t}}}$	REFL	reflexivity of equality
${\displaystyle {\cfrac {\Gamma \vdash s=t\qquad \Delta \vdash t=u}{\Gamma \cup \Delta \vdash s=u}}}$	TRANS	transitivity of equality
${\displaystyle {\cfrac {\Gamma \vdash f=g\qquad \Delta \vdash x=y}{\Gamma \cup \Delta \vdash f(x)=g(y)}}}$	MK_COMB	congruence of equality
${\displaystyle {\cfrac {\Gamma \vdash s=t}{\Gamma \vdash (\lambda x.s)=(\lambda x.t)}}}$	ABS	abstraction of equality (${\displaystyle x}$ must not be free in ${\displaystyle \Gamma }$)
${\displaystyle {\cfrac {\qquad }{\vdash (\lambda x.t)x=t}}}$	BETA	connection of abstraction and function application
${\displaystyle {\cfrac {\qquad }{\{p\}\vdash p}}}$	ASSUME	assuming ${\displaystyle p}$, prove ${\displaystyle p}$
${\displaystyle {\cfrac {\Gamma \vdash p=q\qquad \Delta \vdash p}{\Gamma \cup \Delta \vdash q}}}$	EQ_MP	relation of equality and deduction
${\displaystyle {\cfrac {\Gamma \vdash p\qquad \Delta \vdash q}{(\Gamma -\{q\})\cup (\Delta -\{p\})\vdash p=q}}}$	DEDUCT_ANTISYM_RULE	deduce equality from 2-way deducibility
${\displaystyle {\cfrac {\Gamma [x_{1},\ldots ,x_{n}]\vdash p[x_{1},\ldots ,x_{n}]}{\Gamma [t_{1},\ldots ,t_{n}]\vdash p[t_{1},\ldots ,t_{n}]}}}$	INST	instantiate variables in assumptions and conclusion of theorem
${\displaystyle {\cfrac {\Gamma [\alpha _{1},\ldots ,\alpha _{n}]\vdash p[\alpha _{1},\ldots ,\alpha _{n}]}{\Gamma [\tau _{1},\ldots ,\tau _{n}]\vdash p[\tau _{1},\ldots ,\tau _{n}]}}}$	INST_TYPE	instantiate type variables in assumptions and conclusion of theorem

This formulation of type theory is very close to the one described in section II.2 of Lambek & Scott (1986).

References

• Lambek, J; Scott, P. J. (1986), Introduction to Higher Order Categorical logic, Cambridge University Press, ISBN 9780521356534

Further reading

• Freek Wiedijk (December 2008), "Formal Proof — Getting Started" (PDF), Notices of the American Mathematical Society, 55 (11): 1408–1414, retrieved 2008-12-14

External links

• Official website

• v
• t
• e

ML programming

Software

Implementations, dialects	Caml OCaml° Eff F*° F#° JoCaml° Reason° Standard ML Alice° Extended ML MLton° Standard ML of New Jersey° (SML/NJ) Dependent ML ATS° Concurrent ML Futhark° Lazy ML MacroML Ur°
Programming tools	Alt-Ergo° Astrée Camlp4° FFTW° Frama-C° Haxe° Marionnet° MTASC° Poplog° Semgrep° SLAM project
Theorem provers, proof assistants	Coq° HOL° HOL Light° Isabelle° LEGO Logic for Computable Functions Matita° Twelf°

• GeneWeb°

Community

Designers	Lennart Augustsson (Lazy ML) Damien Doligez (OCaml) Gérard Huet (Caml) Xavier Leroy (Caml, OCaml) Robin Milner (ML) Don Sannella (Extended ML) Don Syme (F#)

• Thierry Coquand
• Steven G. Johnson
• Christine Paulin-Mohring
• Frank Pfenning
• Simon Thompson

Italics = discontinued

° = Open-source software
Book Category:Family:ML Category:Family:OCaml Category:Software:OCaml