Curry–Howard correspondence

Proofs as programs, propositions as types

The principle that proofs and programs correspond structurally. The core slogan is "proofs as programs, propositions as types" — that is, a proposition is a type, and a proof is a program of that type.

For example, in logic corresponds to the function type A -> B in programming, to product/tuple types, and to sum/union types.

Curry–Howard correspondence

In programming language theory and proof theory, the Curry–Howard correspondence is a direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#External_links

Curry–Howard correspondence

Proofs as programs, propositions as types

Backlinks

Recommendations