Verifying Functional Reactive Programs with Side Effects

Work type
Article
Collaborators
Publication status
Published

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:

Haskell

Work type
Talk slides or board photographs
Publication status
Not for publication

An introductory course to Haskell in German.

 

Ein Haskell-Einführungskurs. Enthält Beamer-Folien und einige Aufgaben mit Lösungen.

Bachelor's thesis - Cartan Geometry and Spin Networks

Work type
Article
Collaborators
Publication status
Published

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.

Noncommutative geometry internal to involutive monoidal dagger categories

Work type
Article
Publication status
In Progress

The notion of finite dimensional spectral triples internal to an involutive monoidal dagger category is defined. It makes the definition of a noncommutative geometry with symmetry quantum group possible. Surprising relations to two-dimensional extended TQFTs with line defects are uncovered.