# Curry-Howard-Lambek correspondence

### From HaskellWiki

Revision as of 03:01, 2 November 2006 by Uchchwhash (Talk | contribs)

**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

Integer</haskell> is inhibited (by the value <hask>42

*proves*the proposition

Integer