Intuitionistic type theory

Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory (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.