War Time Proofs and Futuristic Programs
summary
Claims that Gödel’s Dialectica interpretation gives a concrete Curry–Howard variant and that a categorical construction (given in 1988 and extended since) systematically turns proofs-as-types models into linear logic type theories, with the construction provably yielding linear-logic models from simply-typed/category-theoretic inputs. The talk documents concrete tools used (sequent/natural deduction, categorical semantics, realizability-style translations), shows the construction produces lenses concurrency encodings and even automatic differentiation implementations, and reports successful modern generalizations.
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
35mProof Theory Impressionism: Blurring the Curry-Howard Line
01h 44mAn Introduction to Natural Deduction
11mWhat are Dependent Types
01h 00mProspects for Computer Formalization of Infinite-Dimensional Category Theory
33mTheory and Models of Lambda Calculus Untyped and Typed - Part 5 of 5
10mWhen Does a Program Typecheck?
13mTyped Abstractions for Causal Probabilistic Programming
26m(...) How to turn (Liquid) Haskell into a theorem prover