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中形式化。形式化以句法Kripke逻辑关系为核心，并基于前期工作，建立了主体归约、一致性、归一化以及定义性等式的可判定性等主要元理论性质。我们还证明了分级赋值的代入定理以及归约下分级的保持性。此外，我们研究了一种提取函数，它可将项转换为无类型λ-演算并移除可擦除内容，特别是带有“可擦除”分级的函数参数。对于某类模态，我们证明了提取的可靠性能：自然数类型程序在提取前后具有相同的值。对于开放式程序，只要上下文所有变量均为可擦除、上下文一致，且弱Σ-类型不允许擦除匹配，则提取的可靠性同样成立。