一句话：提出静默模态与守卫递归类型的 Curry 式 λ 演算，由编译器控制递归，保证归一化并支持类型推断。
本文研究如何控制无限结构上递归函数式程序的行为。现有方法通常依赖语法中显式的模态标记来指示模态引入/消去规则的应用，本文将这种模态设计为“静默”的，即程序语法中不含任何标记，从而把控制递归的责任从程序员转移给编译器。为此，作者提出一种 Curry 风格的带类型 λ 演算，包含静默模态和守卫递归类型。其类型规则保证了程序的归一化，并且该类型系统可以转化为一种算法，自动推断程序的类型。这一工作为在编译器层面管理递归提供了理论基础。
We investigate the interplay between a modality for controlling the behaviour of recursive functional programs on infinite structures which are completely silent in the syntax. The latter means that programs do not contain "marks" showing the application of the introduction and elimination rules for the modality. This shifts the burden of controlling recursion from the programmer to the compiler. To do this, we introduce a typed lambda calculus a la Curry with a silent modality and guarded recursive types. The typing discipline guarantees normalisation and can be transformed into an algorithm which infers the type of a program.Comment: 32 pages 1 figure in pdf format