Graded Modal Dependent Type Theory with Universe and Erasure - Formalized

Explore a 30-minute conference talk from ICFP 2023 that presents a graded modal type theory with a universe and erasure, fully formalized in Agda. Delve into the theory's features, including Π-types, weak and strong Σ-types, natural numbers, an empty type, and a universe, as well as extensions with a unit type and graded Σ-types. Examine how the theory is parameterized by a modality, allowing for different grade systems to track variable usage in terms and types. Focus on the erasure modality for marking function arguments as erasable. Learn about the formalization's meta-theoretic properties, including subject reduction, consistency, normalization, and decidability of definitional equality. Investigate the extraction function that translates terms to an untyped λ-calculus and removes erasable content. Understand the conditions under which extraction is proven sound for a certain class of modalities. Access supplementary materials, including the article and archive, to further explore this advanced topic in dependent type theory and formal verification.