Diamonds are not forever:
Liveness in Reactive Programming with Guarded Recursion
IT University of Copenhagen
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 our recent paper[1] 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.
In this talk I will give an overview of our submodal approach and
the main results of our paper.
[1]: Bahr. et. al.: Diamonds are not forever: Liveness in
Reactive Programming with Guarded Recursion.