November 2017
Intermediate to advanced
670 pages
17h 35m
English

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.
Read now
Unlock full access