A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
Conference Paper
Formal Antecedent
Foundations and Logic
Citation
Andreas Abel and Nils Anders Danielsson and Andrea Vezzosi. (2023). A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized. Proceedings of the ACM on Programming Languages (ICFP). 7.
Why this reference is included
Abel, Danielsson, and Vezzosi’s A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized (2023) is a key conference paper that the program draws on as a technical source. Cited 3 times in Book I (Categorical Foundations), Part 18, Chapter The Enrichment Frontier, where the program draws on it in the context of “Abel et al. develop graded modal dependent type theory, where a semiring of grades controls variable usage.”
Cited in
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
Abel et al. develop graded modal dependent type theory, where a semiring of grades controls variable usage
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
Resource-sensitive type theory exists (graded modal DTT , substructural DTT )
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
In the enrichment-frontier table across E₀→E₁→E₂→E₃, Abel's graded modal DTT appears as the closest precedent for the E₁→E₂ transition (alongside Joyal arithmetic universes), with the remaining gap being that linear DTT is not yet complete and lacks internal cut-elimination. Book III proposes to attempt what has not been done before.