一句话：提出 Async RaTT，一种带异步延迟模态的异步 FRP 语言，并证明因果性、生产性与无空间泄漏等操作性质。
现有基于模态类型的函数反应式编程（FRP）语言多依赖全局时钟上的延迟模态，但全局时钟对某些应用不自然，会导致抽象泄漏和低效；已有的无全局时钟模态语言又缺乏操作性质证明。本文提出 Async RaTT，一种面向异步 FRP 的新模态语言，核心是异步延迟模态：运行时每个输出通道可关联其依赖的输入通道集合，从而仅在必要时计算新输出。作者给出将完整程序映射为异步输入/输出信号机器的操作语义，并证明因果性、生产性和无空间泄漏。类型系统还能静态确定各输出通道依赖输入集合的上界，尽管该集合在运行时可能变化。
Over the past decade, a number of languages for functional reactive programming (FRP) have been suggested, which use modal types to ensure properties like causality, productivity and lack of space leaks. So far, almost all of these languages have included a modal operator for delay on a global clock. For some applications, however, a global clock is unnatural and leads to leaky abstractions as well as inefficient implementations. While modal languages without a global clock have been proposed, no operational properties have been proved about them, yet. This paper proposes Async RaTT, a new modal language for asynchronous FRP, equipped with an operational semantics mapping complete programs to machines that take asynchronous input signals and produce output signals. The main novelty of Async RaTT is a new modality for asynchronous delay, allowing each output channel to be associated at runtime with the set of input channels it depends on, thus causing the machine to only compute new output when necessary. We prove a series of operational properties including causality, productivity and lack of space leaks. We also show that, although the set of input channels associated with an output channel can change during execution, upper bounds on these can be determined statically by the type system.