Curry-Howard Isomorphism

Independently by Haskell Curry and William Alvin Howard and Nicolas de Bruijn a correspondence between logic an computation in general, and Natural Deduction and Lambda Calculus in particular has been discovered.

References: