The Curry-Howard correspondence is the observation that systems of formal logic and systems of typed computation share the same structure. Propositions correspond to types, proofs correspond to programs, and the process of checking a proof corresponds to type-checking a program. The correspondence is also called “propositions as types.”
Haskell Curry first noticed that the types of combinators in combinatory logic mirror the axioms of implicational logic. William Alvin Howard later extended the observation to natural deduction and the simply typed lambda calculus, showing that proof normalization corresponds to program evaluation.
The correspondence connects three fields: logic (what can be proved), type theory (what can be typed), and category theory (what can be constructed). Extending it further, one arrives at the slogan “proofs as programs, propositions as types, cut elimination as computation.”
In the formal architecture of this vault, the semiotic universe pairs a complete Heyting algebra with a typed lambda calculus. The types of the lambda calculus are drawn from the Heyting algebra of judgements. This is the Curry-Howard correspondence at work: constructing a term of a given type amounts to producing a proof of the corresponding proposition.
Proof assistants such as Lean, Coq, and Agda implement the Curry-Howard correspondence directly. Writing a proof in these systems is writing a program, and the type checker verifies that the proof is correct.