Intuitionistic Type Theory

Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher, in 1972. Martin-Löf has modified his proposal a few times; his 1971 impredicative formulation was inconsistent as demonstrated by Girard's paradox. Later formulations were predicative. He proposed both intensional and extensional variants of the theory.

Intuitionistic type theory is based on a certain analogy or isomorphism between propositions and types: a proposition is identified with the type of its proofs. This identification is usually called the Curry–Howard isomorphism, which was originally formulated for intuitionistic logic and simply typed lambda calculus. Type Theory extends this identification to predicate logic by introducing dependent types, that is types which contain values. Type Theory internalizes the interpretation of intuitionistic logic proposed by Brouwer, Heyting and Kolmogorov, the so called BHK interpretation. The types of Type Theory play a similar role to sets in set theory but functions definable in Type Theory are always computable.

Read more about Intuitionistic Type Theory:  Connectives of Type Theory, Formalisation of Type Theory, Categorical Models of Type Theory, Extensional Versus Intensional, Implementations of Type Theory

Famous quotes containing the words type and/or theory:

    Under the species of Syndicalism and Fascism there appears for the first time in Europe a type of man who does not want to give reasons or to be right, but simply shows himself resolved to impose his opinions.
    José Ortega Y Gasset (1883–1955)

    The whole theory of modern education is radically unsound. Fortunately in England, at any rate, education produces no effect whatsoever. If it did, it would prove a serious danger to the upper classes, and probably lead to acts of violence in Grosvenor Square.
    Oscar Wilde (1854–1900)