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
etch1.3 @p1.2cmp3.0cmp3.0cmp2.3cm@ →prule Transition & Closest Precedent & Remaining Gap & τ Feature , E_0 → E_1 & Altenkirch–Kaposi 2016 ; Bocquet–Kaposi–Sattler 2023 & Non-Boolean, constructive adaptation to four-valued Ω_τ & Earned topos E_τ (I.D59) , E_1 → E_2 & Joyal arithmetic universes ; Abel graded modal DTT & Linear DTT not yet complete; no internal cut-elimination & 5 diagonal discipline; three-grade semiring , E_2 → E_3 & Willard 2001 (weak); Girard TX (fragments) & No full system at CIC-level proof-theoretic strength & *-autonomous proof theory via 5 (I.T39) , Book III proposes to attempt something that has not been done before