Intuitionistic type theory
Introduced by the Swedish philosopher Per Martin-Löf in 1972 as a constructive foundation of mathematics in the tradition of Intuitionism, Intuitionistic Type Theory is at the same time a mathematical language and a programming language. Central is the identification of propositions and types.
A number of computer proof systems have been based on Intuitionistic Type Theory: NuPRL, LEGO, COQ and others.
Referenced By
Intuitionism | Intuitionism (philosophy of mathematics) | MathematicalIntuitionism | Mathematical intuitionism | Neointuitionism
|
