29.11.14
Propositions as Types, with Howard on Curry-Howard
Propositions as Types
Philip Wadler
Draft, 29 November 2014
The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.Comments still solicited!
Labels: Functional Programming, Logic, Programming Languages, Types
Comments:
<< Home
The title of the appendix in this version is "Curry on Curry-Howard" instead of "Howard on Curry-Howard". Is that a typo?
It's interesting that Curry and Mac Lane were the only two Americans who did their doctorates in pre-war Gottingen, both in mathematical logic. Curry's advisor was Hilbert himself, and Mac Lane's was Hilbert's student Hermann Weyl. Although they apparently missed overlapping at Gottingen by a few months, Mac Lane mentions knowing about Curry in his historical essay about his experiences at Gottingen. Perhaps it's not so surprising after all that many years later you and Moggi found deep connections between Curry's work and Mac Lane's work.
It's interesting that Curry and Mac Lane were the only two Americans who did their doctorates in pre-war Gottingen, both in mathematical logic. Curry's advisor was Hilbert himself, and Mac Lane's was Hilbert's student Hermann Weyl. Although they apparently missed overlapping at Gottingen by a few months, Mac Lane mentions knowing about Curry in his historical essay about his experiences at Gottingen. Perhaps it's not so surprising after all that many years later you and Moggi found deep connections between Curry's work and Mac Lane's work.
# posted by 
: 30/11/14 3:13 AM
: 30/11/14 3:13 AM
The Howard->Curry typo is particularly embarrassing! Typos now fixed, with an acknowledgment to Gale. Please let me know if you spot others, and leave your name to be acknowledged.
One but last sentence in section 8: "Rewriting each of these yields the third proof, which derives the term of type A × B, and can be evaluated no further."
Should "proof" be "program" in this sentence?
Post a Comment
Should "proof" be "program" in this sentence?
# posted by : 16/6/15 10:45 PM
: 16/6/15 10:45 PM << Home
