An observation, foundational to type theory, that a precise structural correspondence exists between logical proofs and computer programs, and between logical propositions and types, so that constructing a proof of a proposition corresponds exactly to writing a program of the matching type.
Facts
Core PrincipleA direct relationship between computer programs and mathematical proofs. 1 Connections
In Field
Invented
Haskell Curry observed the correspondence between combinatory logic and intuitionistic logic in the 1930s that gives the correspondence half its name.
Sources
1. Wikipedia: Curry-Howard correspondence
Origins section
In 1934, Curry observes that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic.
Lead, first sentence
is a direct relationship between computer programs and mathematical proofs.
View the SourceReader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.