一句话：提出面向 Curry 风格语言的语法导向子类型框架，用带大小不变量的（余）归纳类型证明递归程序终止。
本文提出一个面向 Curry 风格类型系统、以语法为导向的子类型框架，旨在以较简单的理论与实现支持丰富特性。系统包含和类型、积类型、全称与存在量化，以及归纳与余归纳类型；后两者可携带大小不变量，用于证明递归程序终止，例如通过说明 quicksort 的分区不增加列表大小来推出其终止。关键思想是将大小与递归分离：不直接检查程序终止，而是证明其循环类型推导良基，再借助标准语义归一化证明得到终止。系统可处理归纳与余归纳混合、多态与（余）归纳混合的复杂程序。作者实现了该系统，并接受文中所有示例，说明其可行性。
We present a new, syntax-directed framework for Curry-style type systems with subtyping. It supports a rich set of features, and allows for a reasonably simple theory and implementation. The system we consider has sum and product types, universal and existential quantifiers, and inductive and coinductive types. The latter two may carry size invariants that can be used to establish the termination of recursive programs. For example, the termination of quicksort can be derived by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed polymorphism and (co-)induction. One of the key ideas is to separate the notion of size from recursion. We do not check the termination of programs directly, but rather show that their (circular) typing proofs are well-founded. Termination is then obtained using a standard (semantic) normalisation proof. To demonstrate the practicality of the system, we provide an implementation accepting all the examples discussed in the article.
DOI 原文 ·
@article{paperbot717,
title = {Practical Subtyping for Curry-Style Languages},
author = {Rodolphe Lepigre and Christophe Raffalli},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {41},
number = {1},
year = {2019},
doi = {10.1145/3285955}
}