Intuitionistic type theory
Alternative foundation of mathematics / From Wikipedia, the free encyclopedia
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory, the latter abbreviated as MLTT) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.