Propositions as Types, with Howard on Curry-Howard

Propositions as Types has been updated, again. Thanks again to all the readers and reviewers who helped me improve the paper. This version includes an appendix, Howard on Curry-Howard, including additional correspondence with Howard not previously published.

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: , , ,

Minor typo in the last sentence of section 2: "as describe by Vardi [60]."
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.
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?
Thanks! Typo fixed, with acknowledgment to Blok.
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?