一句话：提出 GraD 分级依赖类型系统，并给出基于堆的使用感知语义与资源核算可靠性证明。
分级类型论（graded type theory）能够跟踪并推理类型系统中的资源使用，但标准操作语义通常不感知资源，使资源核算的正确性难以直接说明。本文提出 GraD：一种新的分级依赖类型系统，涵盖函数、张量积、加和类型与单位类型，并为其设计基于堆的操作语义。作者证明了一个可靠性定理，表明系统能正确核算资源使用。由此可推出若干性质，包括标准类型可靠性、无关（irrelevant）资源不干扰计算，以及线性资源的单指针性质。该工作为在 Haskell 等实用语言中整合线性、无关性与依赖类型奠定了基础。
Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive sums, and a unit type. Since standard operational semantics is resource-agnostic, we develop a heap-based operational semantics and prove a soundness theorem that shows correct accounting of resource usage. Several useful properties, including the standard type soundness theorem, non-interference of irrelevant resources in computation and single pointer property for linear resources, can be derived from this theorem. We hope that our work will provide a base for integrating linearity, irrelevance and dependent types in practical programming languages like Haskell.
@article{paperbot1149,
title = {A graded dependent type system with a usage-aware semantics},
author = {Pritam Choudhury and Harley Eades III and Richard A. Eisenberg and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434331}
}