CurryHowardLambek

The Curry-Howard-Lambek correspondence is a foundational set of ideas linking logic, computation, and category theory. It articulates a tight symmetry between propositions, proofs, and programs, and between types, terms, and morphisms.

The correspondence is named after Haskell Curry and William Alvin Howard, who showed that intuitionistic logic corresponds to a typed lambda calculus: propositions can be viewed as types, and proofs as programs. During the same period, Joachim Lambek extended these ideas into a category-theoretic framework, showing that the typed lambda calculus has a natural interpretation in Cartesian closed categories. The combined perspective is often called the Curry-Howard-Lambek correspondence or isomorphism.

In concrete terms, a proposition corresponds to a type, a proof to a program (or term), and the process of normalizing a proof to the execution of a program. The simply typed lambda calculus is categorical in nature: its terms correspond to morphisms in a Cartesian closed category, and beta-reduction aligns with cut-elimination in logic. Dependent types and richer logics extend the correspondence to more general categorical settings, such as locally cartesian closed categories and toposes, where the internal logic reflects higher-order intuitionistic reasoning.

Impact and applications are broad: the correspondence underpins modern type systems in functional programming languages (for example, ML and Haskell), and informs the design of proof assistants and formalized mathematics through dependent type theories and categorical semantics. It provides a unifying lens for understanding computation, logic, and mathematics.