nLab HOL

Idea

HOL (short for higher-order logic) is a kind of simply typed lambda calculus. There are various 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

proof assistants:

based on plain type theory/set theory:

• Metamath

• Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

• Coq, Agda, Lean, Arend

based on cubical type theory:

• cubicaltt

• redtt

• yacctt

• RedPRL

• Cubical Agda

  • library and demos

  • 1lab (cross-linked reference resource)

based on modal type theory:

• Agda-flat: installation instructions

based on simplicial type theory:

• Rzk

For monoidal category theory:

• DisCoPy

For higher category theory:

• opetopic type theory

• Globular, homotopy.io

projects for formalization of mathematics with proof assistants:

• Archive of Formal Proofs (using Isabelle)

• ForMath project (using Coq)

• MathScheme

• UniMath project (using Coq and Agda)

• Xena project (using Lean)

Other proof assistants

• Andromeda

Historical projects that died out:

• The QED Project

References

• T. Nipkow, L. Paulson, M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, Springer (2002)

• Wikipedia, HOL (proof assistant)

• Florian Rabe and Mihnea Iancu, A Formalized Set-Theoretical Semantics of Isabelle/HOL (pdf)

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