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

### Other related articles:

**Curry–Howard Correspondence**- Other Applications

... genotypes (the program trees evolved by the GP system) by their

**Curry–Howard**isomorphic proof (referred to as a species) ...