一句话：提出带守卫递归与余归纳类型的 λ-演算，保证良类型程序的生产力，并给出指称语义与程序逻辑。
论文面向余归纳类型中递归定义的生产力与推理问题，提出守卫 λ-演算：在简单类型 λ-演算上加入守卫递归类型和余归纳类型。守卫递归类型保证良类型程序的生产力，并借助受模态逻辑与 Atkey-McBride 时钟量化启发的类型构造子，将守卫递归类型转化为余归纳类型，从而支持非因果函数的类型化。作者给出 call-by-name 操作语义，并在树拓扑斯中构造充分的指称语义；充分性证明蕴含程序求值必然终止。论文还引入带 Löb 归纳的程序逻辑，用于推理程序的上下文等价，并通过定义 Rutten 行为微分方程的解展示其表达力。
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with L\"ob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Rutten's behavioural differential equations.
@article{CloustonBGB16,
title = {The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types},
author = {Ranald Clouston and Aleš Bizjak and Hans Bugge Grathwohl and Lars Birkedal},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 3},
year = {2017},
doi = {10.2168/lmcs-12(3:7)2016}
}