Type Theories for Reactive Programming

Christian Uldal Graulund

Research output: Book / Anthology / Report / Ph.D. thesisPh.D. thesis


Functional reactive programming is the application of techniques from functional programming to the domain of reactive programming. In recent years, there has been a growing interest in modal functional reactive programming.
Here, modal types are added to languages for functional reactive programming, with the goal of allowing the type system to enforce properties particular to reactive programming. These include causality, productivity and ruling out so-called spaceleaks.
The main goal of this dissertation has been to develop calculi for modal functional reactive programming, with the final aim being a fully dependent type theory for reactive programming, namely, Reactive Type Theory (RaTT). Such a system would allow a programmer to specify and verify advanced specifications for reactive systems.
The work presented here can be split into two parts: The first is concerned with Fitch-style modal calculi for synchronous (or stream based) functional reactive programming using guarded recursion and their semantics. The second describes a more domain specific modal calculus for asynchronous (or event based) functional reactive programming with widgets.
In chapter 2, the language Simply RaTT is described, which is a simply typed Fitch-style modal language for reactive programming. Both the type system and operational semantics is presented, and we prove that a well-typed term will run in the operational semantics. A special feature of the operational semantics is the aggressive garbage collection algorithm, which ensure that well-typed programs are free of unintended spaceleaks. It is further proved that the language is both causal and productive.
In chapter 3, categorical semantics for Simply RaTT is presented. The model is a Kripke-style presheaf category over a suitable category of worlds. We show that values are interpreted as coalgebras over a garbage collection modality.
To interpret the ○ and □ modality, we use two pairs of adjoint functors. To interpret the fix point operator, we use step-indexing. Finally, we show how terms are interpreted using a reader-like monad.
In chapter 4, the language Lively RaTT is described, which is an extension of Simply RaTT. The main addition is that of temporal inductive types, which can be used to encode termination and liveness. This gives a type system that can be considered as corresponding to intuitionistic linear temporal logic, which
is the natural setting for specifications of reactive properties. In particular, we show that by using a sub-modal approach, we can include temporal inductive types while retaining the ease of programming afforded by guarded recursion.
In chapter 5, the language λWidget is presented. This is a more domain specific language, aimed at programming with widgets at the abstraction level of scene graph, e.g., the DOM in a browser. This language is asynchronous and based around programming with events, and designed to have an efficient implementation strategy. The language provides a novel semantics for widgets and has a natural logical interpretation.
Original languageEnglish
PublisherIT-Universitetet i København
Number of pages129
ISBN (Print)978-87-7949-045-1
Publication statusPublished - 2021


Dive into the research topics of 'Type Theories for Reactive Programming'. Together they form a unique fingerprint.

Cite this