Curry, Howard, and Lambek (CHL) discovered the one-to-one correspondence between objects in category theory, propositions in logic, and types in programming languages.
CHL looked at the types of rules for natural deduction rules and typed Lambda calculus and discovered that they are identical.
If we remove the red terms in the preceding table, they are identical. Hence, Church's lambda types correspond one-to-one with Gentzen's logical formulas. Type checking is the same as proof checking.
- Logic includes ...
