War Time Proofs and Futuristic Programs
summary
Claims that Gödel’s Dialectica interpretation yields a concrete type‑theory bridge to linear logic and that the 1940s construction can be modeled categorically. Provides a categorical construction (original model from 1988) that turns prenex ∃u ∀x AD formulas into objects, maps proofs and counterexamples back and forth as lenses, and produces a model of linear logic type theory. Shows extensions, implementations, and applications (concurrency, linear types, automatic differentiation) and that the method actually generalizes.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 4:47Changing mental models
- 9:46Revolution in the sky
- 10:0820th century math revolution
- 13:20Curry-Howard correspondence
- 17:36Hilbert’s program foundations
- 21:11Natural deduction and sequent calculus
- 22:58Gödel’s wartime proofs
- 24:47Church-Turing thesis
- 26:55Curry-Howard in modern programming
- 28:03Category theory as algebra
- 30:56Gödel’s Dialectica in categories
- 37:25Dialectical categories
- 39:54Conclusion
related talks
01h 12mTruth about Types
57mPropositions as Types
43mPropositions as Types
33mTheory & Models of Lambda Calculus: Typed and Untyped (Part 6)
38mCategory Theory as a Tool for Thought
32mTheory & Models of Lambda Calculus: Typed and Untyped (Part 2)
39mLinear Logic Programming
01h 15mA Crash Course in Category Theory