Diamonds are not forever: Liveness in reactive programming with guarded recursion

Patrick Bahr, Christian Uldal Graulund, Rasmus Ejlers Møgelberg

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


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.
Original languageEnglish
Title of host publicationACM SIGPLAN Symposium on Principles of Programming Languages
Number of pages28
PublisherAssociation for Computing Machinery
Publication dateJan 2021
Publication statusPublished - Jan 2021
SeriesProceedings of the ACM on Programming Languages


  • Functional Reactive Programming
  • Modal Type Systems
  • Guarded Recursion
  • Linear Temporal Logic
  • Curry-Howard Isomorphism


Dive into the research topics of 'Diamonds are not forever: Liveness in reactive programming with guarded recursion'. Together they form a unique fingerprint.

Cite this