Curry–Howard correspondence

en.wikipedia.org · 9,347 words · saved by 1 readers

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

Curry–Howard correspondence - Wikipedia Jump to content From Wikipedia, the free encyclopedia Relationship between programs and proofs \nplus_comm =\nfun n m : nat =>\nnat_ind (fun n0 : nat => n0 + m = m + n0)\n (plus_n_0 m)\n (fun (y : nat) (H : y + m = m + y) =>\n eq_ind (S (m + y))\n (fun n0 : nat => S (y + m) = n0)\n (f_equal S H)\n (m + S y)\n (plus_n_Sm m y)) n\n : forall n m : nat, n + m = m + n\n</syntaxhighlight>"},"content2":{"wt":"A proof of commutativity of addition on natural numbers in the [[proof assistant]] [[Rocq]] (formerly named ''Coq''). {{code |lang=coq |nat_ind}} stands f

Curry–Howard correspondence

related reading