Intuitionistic type theory
From The Art and Popular Culture Encyclopedia
|
Related e |
|
Featured: |
Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory is a type theory and an alternative foundation of mathematics 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.
[edit]
See also
Unless indicated otherwise, the text in this article is either based on Wikipedia article "Intuitionistic type theory" or another language Wikipedia page thereof used under the terms of the GNU Free Documentation License; or on research by Jahsonic and friends. See Art and Popular Culture's copyright notice.
