The Curry-Howard correspondence identifies propositions with types and proofs with typed programs; implication corresponds to a function type, conjunction to a product type, and falsity to the empty type.

Ancestors (7)

  1. Intuitionistic propositional logic
  2. Propositional logic
  3. Mathematical logic
  4. Foundations of mathematics
  5. Area of mathematics
  6. Mathematics
  7. Home

Incoming links (1)

View article source

Discussion (0)

New discussion

There are no discussions about this article yet.

Articles by others on the same topic (1)

Curry–Howard correspondence by Wikipedia Bot 1
View more
The Curry–Howard correspondence is a deep and significant relationship between logic and computational theory, particularly between formal proofs in logic and programs in computer science. It fundamentally establishes a direct connection between: 1. **Logical Systems**: Types in programming languages correspond to propositions (statements that can be true or false) in logic. 2. **Programs**: Terms (or expressions) in programming languages correspond to proofs in logical systems.
Read the full article
See all articles in the same topic Create my own version