Curry–Howard correspondence

The Curry–Howard correspondence links propositions to types, proofs to programs, and proof normalization to computation. It shows how constructive logic and typed programming languages share a formal structure.

Propositional logic: A formal system for expressing and reasoning about propositions using connectives such as conjunction, implication, and disjunction. Its connectives correspond to the basic type constructors used in Curry–Howard.
Propositions as types: The interpretation of logical propositions as types whose inhabitants represent proofs. This is the correspondence’s central assignment from logic to programming.
Proof assistant: Software that helps construct, check, and manage formal mathematical proofs. Proof assistants use typed terms to represent proofs and verify them mechanically.
Haskell Curry: An American mathematician and logician whose work helped establish combinatory logic and foundations of mathematical logic. His name is attached to the correspondence through his work on combinators and implication.
Classical logic: A family of logics that includes the law of excluded middle and double-negation elimination. Its proofs require richer computational interpretations than the basic intuitionistic correspondence.
Type theory: The study of formal systems in which expressions have types that constrain and classify them. Curry–Howard is one of the central bridges between type theory and logic.
Proof term: A formal expression that records the construction of a proof in a proof calculus. Proof terms become programs when deductions are translated into typed expressions.
Curry–Howard–Lambek correspondence: A three-way connection among intuitionistic logic, typed lambda calculi, and Cartesian closed categories. It extends the proposition–type–program pattern by interpreting types categorically.
William Alvin Howard: An American mathematician and logician who formulated the correspondence between natural deduction and typed lambda calculus. Howard’s work made the proof-to-program relationship explicit for natural deduction.
Classical proof: A proof that may use classical principles such as excluded middle or double-negation elimination. Such proofs do not translate directly into ordinary constructive programs without added structure.

Linked from 21 pages