一句话：提出基于类型/大小分析的通用模块化准则，用于证明扩展用户重写规则的单型 λ 演算终止。
本文关注简单类型 λ 演算在加入由用户重写规则定义的函数符号后的终止性。受 Hughes、Pareto 与 Sabry 针对不动点算子和模式匹配函数的工作启发，既有准则常通过类型规则限制函数调用中参数的高度。作者将这一思路推广到基于重写定义的函数，并支持更一般的用户自定义 size 概念，给出通用且模块化的终止性判定准则。该成果为高阶重写系统的终止性证明提供了可组合的类型化方法；摘要未报告实现与实验评估。
Abstract We provide a general and modular criterion for the termination of simply typed λ-calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.