Intuitionistic Type Theory

Intuitionistic type theory (also constructive type theory or Martin-Löf type theory) is a formal logical system and philosophical foundation for constructive mathematics. It is a full-scale system which aims to play a similar role for constructive mathematics as Zermelo-Fraenkel Set Theory does for classical mathematics. It is based on the propositions-as-types principle and clarifies the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic. It extends this interpretation to the more general setting of intuitionistic type theory and thus provides a general conception not only of what a constructive proof is, but also of what a constructive mathematical object is. The main idea is that mathematical concepts such as elements, sets and functions are explained in terms of concepts from programming such as data structures, data types and programs. This article describes the formal system of intuitionistic type theory and its semantic foundations.