The Hitchhiker’s Guide to the Curry-Howard Correspondence by Chris Ford.
From the description:
Slides can be found here: speakerdeck.com/ctford/the-hitchikers-guide-to-the-curry-howard-correspondence
Functions are proofs. Um, I can see how that might work. Go on.
Types are propositions. Really? In what sense?
In fact, a function is the proof of the proposition its type represents. Woah, you’ve lose me now.
Don’t Panic!
The Curry-Howard Correspondence is an elegant bridge between the planet of logic and the planet of programming, and it’s not actually that hard to understand.
In this talk I’ll use the Idris dependently-typed functional programming language for examples, as its type system is sophisticated enough to construct interesting automated proofs simply by writing functions. This talk is not designed to convert you into a theoretical computer scientist, but to share with you a wonderful sight in your journey through the vast and peculiar universe of programming.
A familiarity with functional programming would be useful for appreciating this talk, but it will not require any significant prior study of theoretical computer science.
Great presentation by Chris Ford at EuroClojure!
The only problem I had was coordinating the slides, which aren’t very visible in the presentation, with the slide deck you can download.
Definitely a watch more than once video.
Enjoy!
Useful links (references in the slides):
Edwin Brady, Indris
Edwin Brady, Programming in Indris: A Tutorial
Brian McKenna, EvenOdd in Agda, Idris, Haskell, Scala
Philip Wadler, Propositions as Types (Updated, June 2014)