Linked from

The 21 pages that link to Curry–Howard correspondence, each with the reason it gives.

• Intuitionistic logicRelated: It turns intuitionistic proofs into programs and logical propositions into types.

• Type theoryRelated: It explains why typed terms can represent proofs.

• Natural deductionRelated: Natural-deduction derivations translate into typed lambda terms under this correspondence.

• Sequent calculusRelated: Proof systems related to sequent calculus connect logical derivations with computation.

• Category theoryRelated: Categorical semantics provides structural accounts of logical systems and computation.

• Formal proofRelated: It links formal derivations to executable constructions in typed programming languages.

• Proof theoryRelated: It reveals computational content in formal derivations.

• Mathematical logicRelated: It links proof theory to programming-language design and constructive computation.

• Alonzo ChurchRelated: It extends connections between logic and computation that Church’s formal work helped make precise.

• Lambda calculusRelated: Typed lambda calculus provides a computational interpretation of proof construction.

• IntuitionismRelated: It makes constructive proofs concrete as programs that inhabit proposition-shaped types.

• Proof assistantRelated: It explains why proof assistants can represent mathematical proofs as typed constructions.

• Foundations of mathematicsRelated: It explains why type-theoretic proof assistants can represent both mathematical proofs and computation.

• Law of Excluded MiddleRelated: Under this correspondence, a constructive proof of P ∨ ¬P requires a program deciding P.

• Logical implicationRelated: It interprets implication as a function type that transforms proofs of premises into proofs of conclusions.

• ConstructivismRelated: It turns constructive proofs into computational objects that can yield programs.

• Disjunction introductionRelated: Disjunction introduction corresponds to constructing a value in a sum type.

• Peirce's lawRelated: Under this correspondence, Peirce's law requires control behavior unavailable to ordinary intuitionistic programs.

• Conjunction introductionRelated: Conjunction introduction corresponds to constructing a pair of proofs.

• Deduction theoremRelated: Under this correspondence, implication introduction becomes function construction.

• Cartesian closed categoryRelated: The category's products and exponentials provide categorical counterparts to conjunction and implication.