Type systems and Formal Logic: The Curry–Howard correspondence

Hi guys, I'm talking about the deep and fascinating correspondence between logic and computation in this talk. This is a very "there is no spoon" no kind of topic, which is the kind of thing I think is quite fun to explore. On a practically level it's also pretty much a prerequisite for understanding the principles that modern type inference is built on.

The talk is primarily based around this tutorial on the Curry-Howard correspondence and natural deduction:

http://wellnowwhat.net/papers/ATCHC.pdf

Also relevant

http://en.wikipedia.org/wiki/Natural_deduction http://en.wikipedia.org/wiki/Curry-Howard

See you there!