Works

Published

Verifying Functional Reactive Programs with Side Effects

Collaborators

We develop an embedded domain specific language inside the dependently typed functional programming language Agda for specifying and verifying properties of functional reactive programs. For this purpose, we embed the temporal logic CTL (computation tree logic) inside dependent type theory.

Our EDSL offers all the standard stream programming primitives, and enriches them with two crucial aspects:

Bachelor's thesis - Cartan Geometry and Spin Networks

Collaborators

I went to Erlangen to learn all about Cartan Geometry from Derek Wise. I also learned about spin network quantisation, and we tried to combine the two. Unfortunately we didn't really finish this project. Still, the thesis serves as an introduction to Cartan geometry and some thoughts about quantisation.

Draft

Rhine - FRP with type-level clocks

This article presents Rhine, an FRP library written in Haskell. Both article and implementation are still work in progress, and expected to be finished somewhere in 2017.

In Progress

Preprint