一句话：为λμ演算引入非幂等交并类型系统，用类型推导刻画头/强归一化并给出归约长度上界，并扩展至小步λμs演算。
本文研究经典λμ演算的归一化与资源敏感类型系统。第一部分定义基于非幂等交类型与并类型的两个资源感知类型系统，通过类型推导测度递减的组合论证，刻画头归一化与强归一化项；类型可推导性还为头归约长度和到范式的最大归约序列提供上界。第二部分将λμ演算细化为受“距离替换”启发的小步λμs演算，并给出非幂等解释的自然扩展；在扩展类型系统中，λμs归约保持并减小类型推导。由此得到强λμs归一化项的简单算术刻画。
In the first part of this paper, we define two resource aware typing systems for the {\lambda}{\mu}-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head reduction and the maximal reduction sequences to normal-form. In the second part of this paper, the {\lambda}{\mu}-calculus is refined to a small-step calculus called {\lambda}{\mu}s, which is inspired by the substitution at a distance paradigm. The {\lambda}{\mu}s-calculus turns out to be compatible with a natural extensionof the non-idempotent interpretations of {\lambda}{\mu}, i.e., {\lambda}{\mu}s-reduction preserves and decreases typing derivations in an extended appropriate typing system. We thus derive a simple arithmetical characterization of strongly {\lambda}{\mu}s-normalizing terms by means of typing.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KesnerV19,
title = {Non-idempotent types for classical calculi in natural deduction style},
author = {Delia Kesner and Pierre Vial},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:3)2020}
}