Next | Types Are Theorems; Programs Are Proofs | 31 |

The logic described here is

**intuitionistic**logic (“IL”)It is weaker than

**classical**logic (“CL”)For example, it does not prove

*p* ∨ ¬*p*

(It

**does**prove ¬¬(*p*∨ ¬*p*))Another theorem of classical logic that it doesn't prove is:

((*p* → *q*) → *p*) → *p*

If you add this to IL as an axiom, IL proves everything that CL does

This is the type of

`call/cc`!If you add to Haskell a

`call/cc`function, it becomes a classical logicYou can then construct a value of type

*p*∨ ¬*p*

Next | Next |