In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and proofs. It is a 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.
Read more about Curry–Howard Correspondence: Origin, Scope, and Consequences, General Formulation, Correspondence Between Hilbert-style Deduction Systems and Combinatory Logic, Correspondence Between Natural Deduction and Lambda Calculus, Correspondence Between Classical Logic and Control Operators, Sequent Calculus, Examples, Other Applications