论文标题
带有用法感知语义的级别依赖类型系统（扩展版本）
A graded dependent type system with a usage-aware semantics (extended version)
论文作者
论文摘要
分级类型理论提供了一种机制来跟踪类型系统中资源使用情况的理由。在本文中，我们开发了Grad，这是一种新型的级别依赖类型系统的新颖版本，其中包括功能，张量产品，添加剂和单位类型。由于标准操作语义是资源 - 敏捷的，因此我们开发了基于堆的操作语义，并证明了一种合理的定理，显示了对资源使用情况的正确计算。可以从该定理得出几种有用的属性，包括标准类型的音质定理，计算中不相关资源的不相关资源以及线性资源的单个指针属性。我们希望我们的工作将为整合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.
