Types as propositions, programs as proofs
The Curry-Howard correspondence, part 1
Tags: functional, math, logic