# Curry-Howard-Lambek correspondence

From HaskellWiki

Revision as of 03:01, 2 November 2006 by Uchchwhash (talk | contribs) (starting a semi-project, need help! (especially for Indexed Types))

**Curry-Howard Isomorphism** is an isomorphism between types (in programming languages) and propositions (in logic). Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs (and *vice versa*).

## Contents

## The Answer

As is well established by now,

```
theAnswer :: Integer
theAnswer = 42
```

The logical interpretation of the program is that the type `Integer</haskell> is inhibited (by the value <hask>42`

), so the existence of this program *proves* the proposition `Integer`

(a type without any value is the "bottom" type, a proposition with no proof).