Curry–Howard correspondence

Definition

Consider intuitionistic propositional logic in natural deduction, with implication, conjunction and disjunction. Consider the simply typed lambda calculus with function types $A \to B$, product types $A \times B$ and sum types $A + B$. The Curry–Howard correspondence is the map between the two systems given by these clauses.

1. A formula is read as a type: $A \to B$ as the function type, $A \wedge B$ as $A \times B$, and $A \vee B$ as $A + B$.
2. An assumption $A$ with label $x$ is read as a variable $x : A$.
3. Each introduction rule is read as a term constructor: $\to$-introduction as $\lambda$-abstraction, $\wedge$-introduction as pairing, and $\vee$-introduction as an injection.
4. Each elimination rule is read as a destructor: $\to$-elimination as application, $\wedge$-elimination as a projection, and $\vee$-elimination as case analysis.

Under this map, a derivation of $B$ from assumptions $A_1, \dots, A_n$ corresponds to a term $M$ with $x_1 : A_1, \dots, x_n : A_n \vdash M : B$, and conversely. A detour in a derivation is an introduction followed at once by an elimination. It corresponds to a redex, and removing the detour corresponds to one reduction step, such as $(\lambda x.\, M) N \to M[N/x]$.