一句话：提出 Fitch 风格模态演算 Simply RaTT，保证反应式程序因果性并消除空间与时间泄漏。
函数式反应式编程（FRP）需要保证程序因果性，并避免空间泄漏与时间泄漏。已有工作用模态类型在同步 FRP 中提供对信号和事件的直接访问，但多采用双上下文（dual context）风格，类型系统较复杂，且仍存在时间泄漏。本文提出 Simply RaTT：一种采用 Fitch 风格模态类型的反应式编程演算。该风格简化了类型系统，使程序更简洁。作者给出操作语义，可安全执行程序而不产生空间泄漏；同时识别出其他模态 FRP 语言中由延迟计算里不动点展开引起的时间泄漏来源，并证明 Fitch 风格展示能自然排除这类泄漏，而传统双上下文方法似乎难以做到。
Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For this to make sense, an FRP language must ensure that all programs are causal, and can be implemented without introducing space leaks and time leaks. To this end, some FRP languages do not give direct access to signals, but just to signal functions. Recently, modal types have been suggested as an alternative approach to ensuring causality in FRP languages in the synchronous case, giving direct access to the signal and event abstractions. This paper presents Simply RaTT , a new modal calculus for reactive programming. Unlike prior calculi, Simply RaTT uses a Fitch-style approach to modal types, which simplifies the type system and makes programs more concise. Echoing a previous result by Krishnaswami for a different language, we devise an operational semantics that safely executes Simply RaTT programs without space leaks. We also identify a source of time leaks present in other modal FRP languages: The unfolding of fixed points in delayed computations. The Fitch-style presentation allows an easy way to rules out these leaks, which appears not to be possible in the more traditional dual context approach.
@article{paperbot601,
title = {Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks},
author = {Patrick Bahr and Christian Uldal Graulund and Rasmus Ejlers Møgelberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341713}
}