Skip to content
Hallway
0:00 / 0:00

#curry-howardisomorphism#propositionsastypes#haskell

Philip Wadler - Propositions as Types (Lambda Days 2016)

Erlang Solutions

18K subscribers • 48 videos on Hallway

YouTube
  • Recommended by 2 people: 2 on Hacker News.
  • A classic. People kept recommending it from 2016 to 2021.
  • Presented by Philip Wadler, co-designer of Haskell

Intermediate. Assumes working knowledge.

20K views10 years ago2 recommendations

Programming languagesComputer scienceLanguage design and type systemsFunctional programmingComputation and complexity

Philip Wadler explains the Curry-Howard isomorphism, linking formal logic propositions to programming language types.

Slides and more info: lambdadays.org/lambdadays2... Alternative recording: youtube.com/watch?v=IOiZatlZtGU 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. Learn why functional programming is (and is not) the universal programming language.

Why it's here

2 people recommend this

What people say. Recommended as an excellent explanation of the Curry-Howard correspondence and the relationship between types and proofs.

Moments people linked to

vishnuguptaon Hacker News • Recommends

On ““Computer science is not about computers””

I suggest a combination of theory (videos/books/papers) and practice. For practice; I highly recommend learning Haskell. If you are new to functional programming then learning Haskell is challenging and frustrating but as with any new topic the key is to not give up but keep probing. A good recent development is lot of mainstream languages are beginning to include functional paradigms such as lambda, closures etc., For example Java introduced lambda expressions, Javascript has had them for a while now. But from a first-principles stand point Haskell is as good as it gets so please do learn and code in Haskell if not at work then at least side projects. For theory I've found following materia…
View on Hacker News

knucklesandwichon Hacker News • Recommends

On “Type Wars”

> Neither is static typing. It's a layer of protection, much like tests. Not true. The curry-howard correspondence shows the relationship between typed programs and proofs. I recommend you watch a Phillip Wadler talk about this: link to this video Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers. > I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will catch type errors in a dynamically typed language that a statically typed language picked up at compile time.. This isn't necessarily true unless you test for all inputs (which tends to be…
View on Hacker News

u/mn-haskell-guyin r/haskell • Mentions

On “Category Theory for the Working Hacker”

Other (recent) appearance of Lambda Man: link to this video link to this video link to this video link to this video link to this video link to this video link to this video
13View on Reddit

irfansharifon Hacker News • Mentions

On “A monoid is a category, a category is a monad, a monad is a monoid”

just to note this talk briefly alludes to another subject, the Curry–Howard isomorphism, something Philip Wadler had similarly given a talk about at Lambda Days (2016) titled 'Propositions as Types'1 (slides 2 and the video recording3). 1: link 2: link 3: link to this video
View on Hacker News

u/ruffy_1in r/haskell • Mentions

On “Finding my favourite Haskell t-shirt”

Does anybody know if the "Lambdaman" T-Shirt which Phil Wadler was wearing in one of his talks is available somewhere? 51' 30'' link to this video
2View on Reddit