Propositions as Types
summary
Argues the concrete claim that propositions as types is an exact correspondence: formulas ↔ types, proofs ↔ programs, and normalization = evaluation, not just an analogy. Shows specific tools: untyped and simply‑typed lambda calculus, natural deduction and sequent calculus, System F and Hindley‑Milner, Turing machines and normalization proofs. Notes the striking fact that three independent computability definitions arrive together. Points to built outcomes: terminating typed calculi, CPS compilation, proof assistants and session types for concurrency, and that these actually work in practice.
AI-written summary · about
chapters (14)
- 0:00Start
- 6:56Syntax of Lambda
- 12:44Propositions as Types
- 14:08Introduction Rules
- 14:44Rule for Implication
- 24:52Simplify Proofs
- 26:59Negation
- 29:06Lambda Calculus
- 29:26Typed Lambda Calculus
- 31:05Lambda Expressions
- 31:37Extend Lambda Calculus with a Pairing Operation
- 37:22Curie Howard Isomorphism
- 41:06Polymorphic Lambda Calculus
- 44:23Dependent Types
related talks
43mPropositions as Types
38mPropositions as Types for Beginners in Haskell
41mWar Time Proofs and Futuristic Programs
01h 52mIsomorphic Reasoning: Counting with Types Part 3
33mTheory & Models of Lambda Calculus: Typed and Untyped (Part 6)
01h 39mIsomorphic Reasoning: Counting with Types Part 1
06mLightning Talk: Curry-Howard Correspondence
58mType Theory Behind the Glasgow Haskell Compiler Internals (Part 4)