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

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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstract

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.
OriginalsprogEngelsk
TitelACM SIGPLAN Symposium on Principles of Programming Languages
Antal sider28
Vol/bind5
ForlagAssociation for Computing Machinery
Publikationsdatojan. 2021
UdgavePOPL
DOI
StatusUdgivet - jan. 2021
NavnProceedings of the ACM on Programming Languages

Emneord

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

Fingeraftryk

Dyk ned i forskningsemnerne om 'Diamonds are not forever: Liveness in reactive programming with guarded recursion'. Sammen danner de et unikt fingeraftryk.

Citationsformater