# Curry-Howard isomorphism

> In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation.

<Haskell Curry>와 <William Alvin Howard>에서 따온 이름.

## To read

- https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- https://timothysamson.github.io/posts/curry-howard/
- http://apm.bplaced.net/w/index.php?title=Curry-Howard-Lambeck_isomorphism