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

 

See you there!

Join or login to comment.

7 went

Our Sponsors

  • House 4 Hack

    House 4 Hack is providing us with an awesome venue

  • O'Reilly

    O'Reilly offers member book discounts and review copies of their books.

Imagine having a community behind you

Get started Learn more
Rafaël

We just grab a coffee and speak French. Some people have been coming every week for months... it creates a kind of warmth to the group.

Rafaël, started French Conversation Group

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy