constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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.
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
based on cubical type theory:
based on modal type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq and Agda)
Xena project (using Lean)
Other proof assistants
Historical projects that died out:
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
Last revised on September 12, 2019 at 07:00:05. See the history of this page for a list of all contributions to it.