Propositions as Types, Philip Wadler. Draft, March 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.

Philip Wadler has written a very enjoyable (*Like busses: you wait two thousand years for a definition of â€œeffectively calculableâ€, and then three come along at once*) paper about propositions as types that is accessible to PLTlettantes.

## Recent comments

16 hours 37 min ago

22 hours 32 min ago

1 day 29 min ago

1 day 10 hours ago

3 days 6 hours ago

4 days 13 hours ago

4 days 13 hours ago

6 days 10 hours ago

6 days 22 hours ago

1 week 2 days ago