type represents its proof. Curry-Howard correspondence The Curry–Howard correspondence is the observed similarity between logics and programming languages. The implication in logic, "A B" resembles a function from type "A" to type "B". For a variety of logics, the rules are a similar to expression in a programming language's types. The similarity goes farther, as applications of the rules resemble programs in the programming languages. Thus, the correspondence is often summarized as "proofs as programs". The logic operators "for all" and "exists" led Per Martin-Löf to invent dependent type theory. Intuitionistic logic When some types are interpreted as propositions, there is a set of common types that can be used to connect them to make a logic out of types. However, that logic is not classical logic but intuitionistic logic. That is, it does not have the law of excluded middle nor double negation. There is a natural relation of types to logical propositions. If "A" is a type representing a proposition, being able to create a function of type " A" indicates that A has a proof and being able to create the function "A " indicates that A does not have a proof. That is, inhabitable types are proven and uninhabitable types are disproven. WARNING: This interpretation can lead to a lot of confusion. A type theory may have terms "true" and "false" of type "bool", which act like a Boolean logic, and at the same time have types and to represent "true" (provable) and "false" (disproven), as part of a intuitionistic logic for proposition. Under this intuitionistic interpretation, there are common types that act as the logical operators: But under this interpretation, there is no law of excluded middle. That is, there is no term of type Π A . A + (A ). Likewise, there is no double negation. There is no term of type Π A . ((A ) ) A. (Note: Intuitionistic logic does allow and there is a term of type (((A ) ) ) (A ).) Thus, the logic-of-types is an intuitionistic logic. Type theory is often cited as an implementation of the Brouwer–Heyting–Kolmogorov interpretation. It is possible to include the law of excluded middle and double negation into a type theory, by rule or assumption. However, terms may not compute down to canonical terms and it will interfere with the ability to determine if two terms are judgementally equal to each