Propositions as Types, updated

Propositions as Types has been updated. Thanks to all the readers and reviewers who helped me improve the paper.

Propositions as Types
Philip Wadler
Draft, 26 June 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: , , ,

There are two threads on the homotopy type theory list that may be of interest if you take another pass over this paper:




On the latter, the place to begin reading is Streicher's message of January 15. I believe he address a common misconception, which your paper does not participate in, but nor does it directly challenge -- the idea that since all propositions may be given types, then we must associate all types with propositions. This leads to such silliness as Haskell users being introduced to Curry-Howard asking what the proposition is corresponding to the type of hGetLine. (Ok, sure, this is not entirely silly, but still..).

The former thread also points to a lacunae in your paper, but again one that you are perfectly within your rights to not address -- the unfortunate (in my mind) underplaying of the role of realizability with regards to the notion of "proofs as computations." This is in a sense not directly in the CH lineage the same way BHK is, but nonetheless, it was an important step in a similar direction. Of course your paper is not just a discourse on history, but is a work intended for education and exposition, so this may all be a bit besides the point.
Post a Comment

<< Home

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