Propositions as Types
summary
Claims that Propositions as Types means propositions are types, proofs are programs and proof normalization equals program evaluation, demonstrated by mapping natural deduction rules to the simply typed lambda calculus and the swap example that evaluates by substitution. Tools include normalization proofs, Turing’s termination result for typed terms, and proof assistants built on dependent types such as Agda and Coq. Historical equivalences and a 25–35 year industry adoption lag are shown, and termination in the typed fragment is confirmed.
AI-written summary · about
chapters (22)
- 0:00Introduction
- 1:22David Hilbert
- 1:52Antidual problem
- 2:20Incompleteness theorem
- 4:36Alonzo Church
- 4:55lambda calculus
- 5:55girdle
- 7:07Turing machines
- 7:51Is mathematics invented
- 9:14Natural Deduction
- 12:07Formal Proof
- 12:53Sub Formula Property
- 14:29Example
- 18:21Type Theory
- 21:01Evaluation
- 22:23Holding problem
- 22:57Evaluation of programs
- 24:15History
- 25:36Polymorphic lambda calculus
- 28:33Philosophy
- 31:50Multiverses
- 33:20Questions
related talks
57mPropositions as Types
38mPropositions as Types for Beginners in Haskell
01h 12mTruth about Types
41mWar Time Proofs and Futuristic Programs
33mTheory & Models of Lambda Calculus: Typed and Untyped (Part 6)
06mLightning Talk: Curry-Howard Correspondence
55mProving Theorems and Certifying Programs with Coq
40mType-Driven Program Synthesis