nLab
HOL

Contents

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.

proof assistants:

based on plain type theory/set theory:

based on dependent type theory/homotopy type theory:

For monoidal category theory:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Historical projects that died out:

References