Abstract
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 nal 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 specications
for reactive systems.
The work presented here can be split into two parts: The rst 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 specic 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 x 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 specications 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 aorded by guarded recursion.
In chapter 5, the language Widget is presented. This is a more domain specic 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 ecient implementation strategy. The language provides a novel semantics for widgets
and has a natural logical interpretation.
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 nal 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 specications
for reactive systems.
The work presented here can be split into two parts: The rst 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 specic 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 x 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 specications 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 aorded by guarded recursion.
In chapter 5, the language Widget is presented. This is a more domain specic 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 ecient implementation strategy. The language provides a novel semantics for widgets
and has a natural logical interpretation.
| Originalsprog | Engelsk |
|---|
| Forlag | IT-Universitetet i København |
|---|---|
| Antal sider | 129 |
| ISBN (Trykt) | 978-87-7949-045-1 |
| Status | Udgivet - 2021 |
| Navn | ITU-DS |
|---|---|
| Nummer | 175 |
| ISSN | 1602-3536 |