Intuitionistic type theory

In mathematics and logic, an intuitionistic type theory, or constructive type theory, is, most broadly, any type theory done in accordance with the principles of mathematical constructivism. There is particular interest in pure intuitionistic type theories that can serve as a foundation of mathematics. The first complete attempt was made by Per Martin-Löf , a Swedish mathematician and philosopher, in 1972. Martin-Löf had modified his proposal a few times; any version may be called the Intuitionistic Theory of Types.

Many constructive type theorists, especially those working in foundations, want to develop a type theory can serve at the same time as a mathematical language and a programming language. The Curry Howard isomorphism suggests an identification of propositions and types in intuitionistic logic, so that type theory encompasses the (intuitionistic) predicate calculus, while also providing an alternative to set theory. Because term expressions are built up recursively in type-theoretic derivations, any term (including a proof of a proposition) may be evaluated as a program.

This suggests that type theory may be useful for automated proof-checking, and even automated theorem-proving. A number of computer proof systems have been based on these ideas, including Automath , NuPRL , LEGO , and Coq.