一句话：提出 Lively RaTT，将 LTL 的时间步模态作为守卫递归的子模态，在保留守卫不动点的同时支持活性类型。
针对模态函数反应式编程（FRP）中守卫递归与线性时序逻辑（LTL）类型之间的冲突——守卫不动点会破坏归纳类型提供的终止保证——本文提出将 LTL 的时间步模态视为守卫递归所用模态的子模态，而非等同两者。作者设计了 Lively RaTT：一种既含守卫不动点算子、又含 LTL 式 until 类型构造子的模态 FRP 语言，并展示如何编写事件与公平流程序。利用步进索引的 Kripke 逻辑关系，论文证明了 Lively RaTT 的操作性质，包括生产率与因果性，以及 LTL 类型所期望的终止性与活性；最后证明其类型系统保证不存在隐式空间泄漏。
When designing languages for functional reactive programming (FRP) the main challenge is to provide the user with a simple, flexible interface for writing programs on a high level of abstraction while ensuring that all programs can be implemented efficiently in a low-level language. To meet this challenge, a new family of modal FRP languages has been proposed, in which variants of Nakano's guarded fixed point operator are used for writing recursive programs guaranteeing properties such as causality and productivity. As an apparent extension to this it has also been suggested to use Linear Temporal Logic (LTL) as a language for reactive programming through the Curry-Howard isomorphism, allowing properties such as termination, liveness and fairness to be encoded in types. However, these two ideas are in conflict with each other, since the fixed point operator introduces non-termination into the inductive types that are supposed to provide termination guarantees. In this paper we show that by regarding the modal time step operator of LTL a submodality of the one used for guarded recursion (rather than equating them), one can obtain a modal type system capable of expressing liveness properties while retaining the power of the guarded fixed point operator. We introduce the language Lively RaTT, a modal FRP language with a guarded fixed point operator and an `until' type constructor as in LTL, and show how to program with events and fair streams. Using a step-indexed Kripke logical relation we prove operational properties of Lively RaTT including productivity and causality as well as the termination and liveness properties expected of types from LTL. Finally, we prove that the type system of Lively RaTT guarantees the absence of implicit space leaks.
@article{paperbot1168,
title = {Diamonds are not forever: liveness in reactive programming with guarded recursion},
author = {Patrick Bahr and Christian Uldal Graulund and Rasmus Ejlers Møgelberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434283}
}