Encyclopedia  |   World Factbook  |   World Flags  |   Reference Tables  |   List of Lists     
   Academic Disciplines  |   Historical Timeline  |   Themed Timelines  |   Biographies  |   How-Tos     
Sponsor by The Tattoo Collection
Intuitionistic type theory
Main Page | See live article | Alphabetical index

Intuitionistic type theory

Introduced by the Swedish mathematician and 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.