A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
summary
A graded dependent type theory is formalized in Agda (≈39,000 lines) with Π, weak/strong Σ, Nat, Empty, a universe, and a parameterized semiring‑like modality that records usage grades; proofs establish subject reduction, normalization, decidability of definitional equality, substitution for grade assignment, and preservation of grades under reduction. An extraction pass erases grade‑0 content to an untyped λ‑calculus with a crash token and is proved sound for natural number results for a class of modalities, assuming consistency and no erased matches.
AI-written summary · about
chapters (11)
- 0:00Graded modal dependent type theory
- 1:24Erasure to reduce executable size
- 3:12Formalization in Agda
- 6:43Graded modality structure
- 10:20Usage relation for variables
- 13:49Eliminators and erased arguments
- 17:07Preservation theorem
- 18:12Compiler for erasure
- 20:37Canonicity and pattern matching
- 22:50Graded Sigma and recursive types
- 23:57Q&A
related talks
21mGraded Monoids for Dependently Typed Array Programming
26mAbstraction Functions as Types
52mType Theory and its Meaning Explanations
53mIntroduction to Intuitionistic Type Theory
25mDi- is for Directed: First-Order Directed Type Theory via Dinaturality
49mFinite functional programming via graded effects and relevance types
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code