Intuitionistic_type_theory Intuitionistic_type_theory

Intuitionistic type theory - Definition and Overview

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. Its central idea 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.


E-to-the-i-pi.png 		 This mathematics-related article is a stub. You can help Wikipedia by expanding it (http://www.wordiq.com/definition/Intuitionistic_type_theory).

Example Usage of Intuitionistic
stackexchange: StackExchange: Intuitionistic interpretation of classical logic - http://stackexchangesites.com/c6C
intuitionistic: "The proof of a system's value is its existence." Perlis, más en http://www-pu.informatik.uni-tuebingen.de/users/klaeren/epigrams.html
kpich: Oh man I forgot that every f : R -> R is continuous for the Intuitionistic Reals.
Copyright 2009 WordIQ.com - Privacy Policy  :: Terms of Use  :: Contact Us  :: About Us
This article is licensed under the GNU Free Documentation License. It uses material from the this Wikipedia article.