AI 中文总结
研究为德布鲁因记号下的线性λ演算引入适合的类型系统，其规则类似霍达斯和米勒模型，能保证项的线性且无需出现检查，还确立了归约主题性质。
AI 中文摘要
我们引入了一个特别适合对德布鲁因记号下的线性λ演算进行类型化的系统。此类型规则让人联想到霍达斯和米勒的资源消耗模型，能确保任何良类型项是线性的，无需出现检查。接着我们确立了归约主题性质。
英文摘要
We introduce a typing system that is particularly well suited for typing the linear lambda-calculus in de Bruijn notation. This typing discipline, which is reminiscent of Hodas' and Miller's model of resource consumption, guarantees that any well-typed term is linear without the need for an occurrence check. We then establish the subject reduction property.
CommentsIn Proceedings LSFA 2026, arXiv:2607.15904
Journal refEPTCS 449, 2026, pp. 71-87
