自然推导风格中的经典演算的非幂等类型
摘要：基于非幂等交集和并集类型，本文的第一部分为{lambda}{mu}-lambda演算定义了两个资源感知的类型系统。非幂等方法基于类型推导的渐减度量提供了非常简单的组合论证，用于表征首部规范化和强规范化术语。此外，可类型化性为头部规约的长度和最大规约序列到正规式的长度提供了上界。本文的第二部分将{lambda}{mu}-lambda演算改进为一种小步演算，称为{lambda}{mu}s。该演算受到远程替换范式的启发。{lambda}{mu}s演算与{lambda}{mu}的非幂等解释的自然扩展相兼容，即{lambda}{mu}s规约在扩展的适当类型系统中保持并减少类型推导。因此，我们通过类型推导得到了关于强{lambda}{mu}s规范化术语的简单算术特征化描述。
作者：Delia Kesner and Pierre Vial
论文ID：1802.05494
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22