一句话：提出带自然数递归的分级模态类型论，并在 Agda 中形式化证明资源使用计数可靠，且可扩展到信息流非干涉。
本文研究如何在分级模态类型论中支持自然数递归，同时精确追踪资源使用。作者提出一个参数化的分级模态类型论，其 grade 可实例化为擦除、线性或仿射等使用模式；其自然数消去子足够灵活，可表达不同资源使用模式，并可用 large elimination 编码其他数据类型。核心方法是在 Agda 中形式化该理论及其抽象机器，证明资源使用计数可靠：机器按“正确”次数访问资源。该证明还可适配到追踪信息流的 grade，从而导出非干涉性质。
We present a graded modal type theory with recursion over natural numbers and prove formally in Agda that it handles resources correctly, in the sense that an abstract machine accesses resources the "correct" number of times. The theory is parametrized, and can for instance be instantiated with grades for erasure, linear types, or affine types. The correctness proof shows that our usage counting is sound. Our eliminator for natural numbers is flexible as it enables different resource-usage patterns and practical in the sense that it can be used both to define functions with expected usage counts for the arguments. Further, it can be used to encode other data types, using large elimination. Finally, we adapt our resource correctness proof to show correctness also for grades tracking information flow, in the form of a non-interference property.
@article{ErikssonAD26,
title = {On Recursion in Graded Modal Type Theory},
author = {Oskar Eriksson and Andreas Abel and Nils Anders Danielsson},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828677}
}