We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has $Π$-types, weak and strong $Σ$-types, natural numbers, an empty type, and a universe, and we also extend the theory with weak and strong unit types and graded $Σ$-types. The theory is parameterized by a modality structure, a kind of partially ordered semiring, whose elements (grades) are used to track the usage of variables in terms and types. Different modalities are possible. We focus mainly on quantitative properties, in particular erasure: with the erasure modality one can mark function arguments as erasable. The theory is fully formalized in Agda. The formalization, which uses a syntactic Kripke logical relation at its core and is based on earlier work, establishes major meta-theoretic properties such as subject reduction, consistency, normalization, and decidability of definitional equality. We also prove a substitution theorem for grade assignment, and preservation of grades under reduction. Furthermore we study an extraction function that translates terms to an untyped $λ$-calculus and removes erasable content, in particular function arguments with the "erasable" grade. For a certain class of modalities we prove that extraction is sound, in the sense that programs of natural number type have the same value before and after extraction. Soundness of extraction holds also for open programs, as long as all variables in the context are erasable, the context is consistent, and erased matches are not allowed for weak $Σ$-types.

翻译：我们提出了一种分级模态类型理论，这是一种带有等级标记的依赖类型理论，可用于强制执行代码的多种性质。该理论包含Π-类型、弱Σ-类型与强Σ-类型、自然数、空类型及一个宇宙，并进一步扩展到弱单位类型、强单位类型及分级Σ-类型。该理论以模态结构（一种偏序半环）为参数，其元素（即等级）用于跟踪项和类型中变量的使用情况。不同模态均可适用。我们主要关注量化性质，特别是擦除功能：借助擦除模态，可将函数参数标记为可擦除。该理论已在Agda中完全形式化。该形式化以语法克里普克逻辑关系为核心，基于前期工作构建，确立了主体元理论性质，包括主题归约、一致性、正规化及定义性相等的可判定性。我们还证明了等级赋值的替换定理，以及归约下等级的保持性。此外，我们研究了一种提取函数，该函数将项翻译为无类型λ-演算，并移除可擦除内容（尤其是具有"可擦除"等级的函数参数）。对于特定类别的模态，我们证明了提取的可靠性：即自然数类型的程序在提取前后具有相同的值。对于开放程序，只要上下文中的所有变量均为可擦除、上下文一致，且不允许弱Σ-类型的擦除匹配，提取的可靠性依然成立。