论文标题
线性等级交点类型
Linear Rank Intersection Types
论文作者
论文摘要
非数字交叉点类型提供了有关打字程序的定量信息，并已用于获得时间和空间复杂度度量。交点类型系统表征终止，因此需要限制才能确定典型性。这样的限制是使用有限等级的概念为基于掌握的交叉点类型。在这项工作中，我们为非数字交叉点类型定义了新的等级概念。然后，我们使用等级2的新概念为lambda-calculus定义了一种新型类型系统和类型的推理算法。在这项工作的第二部分中，我们扩展了类型系统和类型推理算法来使用与资源使用相关的非数字相交类型的定量属性。
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to make typability decidable. One such restriction consists in using a notion of finite rank for the idempotent intersection types. In this work, we define a new notion of rank for the non-idempotent intersection types. We then define a novel type system and a type inference algorithm for the lambda-calculus, using the new notion of rank 2. In the second part of this work, we extend the type system and the type inference algorithm to use the quantitative properties of the non-idempotent intersection types to infer quantitative information related to resource usage.
