HOL in nLab

+-- {: .rightHandSide}
+-- {: .toc .clickDown tabindex="0"}
### Context
#### Constructivism, Realizability, Computability
+-- {: .hide}
[[!include constructivism - contents]]
=--
=--
=--


#Contents#
* table of contents
{:toc}

## Idea

_HOL_ (short for [[higher-order logic]]) is a kind of [[simply typed lambda calculus]]. There are various [[proof assistant|proof assistants]] that implement this language. The most known one is _[[Isabelle]]_, that has HOL or Isabelle/HOL as its main application.

Other proof assistants of this kind are HOL4, [[HOL Light]], HOL Zero, and ProofPower.

## Related entries

[[!include proof assistants and formalization projects -- list]]


## References

* T. Nipkow, L. Paulson, M. Wenzel. _Isabelle/HOL &#8212; A Proof Assistant for Higher-Order
Logic_, Springer (2002)

* Wikipedia, _[HOL (proof assistant)](http://en.wikipedia.org/wiki/HOL_%28proof_assistant%29)_

* Florian Rabe and Mihnea Iancu, _A Formalized Set-Theoretical Semantics of
Isabelle/HOL_ ([pdf](https://kwarc.info/people/frabe/Research/RI_isabelle_10.pdf))

*  M. J. C. Gordon and T. F. Melham (editors), _Introduction to HOL: A
Theorem Proving Environment for Higher Order Logic_, 1993

* Michael Norrish and Konrad Slind, *The HOL System LOGIC* ([pdf](https://master.dl.sourceforge.net/project/hol/hol/trindemossen-1/trindemossen-1-logic.pdf?viasf=1))

[[!redirects HOL light]]

[[!redirects HOL4]]