Polynomial Time and Dependent types

on YouTube ↗20m

" summary

Combines two concrete implicit‑P approaches — a cons‑free linear system that bans construction of iterable data, and an LFPL style diamond payment system that charges diamonds for constructors — and lifts them to dependent types via Quantitative Type Theory. Claims: well‑typed terms correspond to realizers that run in polynomial time; soundness is proved by Dal Lago–Hofmann style realizability and a mechanized formalization accompanies the paper. Implements dependent eliminators, defines P/NP/BPP and reductions; does not yet formalize NP‑completeness (requires source reflection).

AI-written summary · about

" chapters (13)

1. 0:00Polynomial time and dependent types
2. 1:07Program complexity accounting
3. 2:53Implicit polynomial time via linear typing
4. 4:57Cons-free system for polynomial time
5. 6:23LFPL with diamond constructors
6. 7:30Linearity with dependent types
7. 8:34Quantitative type theory for resources
8. 10:21Diamond types in linear systems
9. 11:45Realizability types for polynomial time
10. 12:29Complexity classes in the system
11. 13:57Probabilistic class BPP
12. 14:17Conclusion and future directions
13. 15:00Q&A