"Propositions as Types" by Philip Wadler

Why it was recommended

best ~40 minutes I've ever spent.

Strong recommendationimode · Original2017-01

What it covers

Philip Wadler's Strange Loop talk on Propositions as Types, the link between logic and computation (the Curry-Howard correspondence). He traces its history through Church. It is for someone who already knows the basic terms and wants the next step.

Video details

Channel

Strange Loop Conference

Length

42 min 43 sec

Year

2015

More in this topic

• Brian Beckman: Don't fear the Monad
• 28c3: The Science of Insecurity
• Math's Fundamental Flaw
• The Banach–Tarski Paradox
• The Future of Mathematics?
• Leslie Lamport: Thinking Above the Code