Curry-Howard correspondence

The Curry-Howard correspondence is the direct relationship between computer programs and mathematical proofs. Also known as Curry-Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence, it refers to the generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard.

Reference:
http://en.wikipedia.org/wiki/Curry-Howard_isomorphism