About me
I received my PhD at the Programming Languages and Compiler Construction group at the University of Kiel in February 2020. My main interest lies in functional programming. This interest comes in different flavours.
Research
The FreeProving projects aims at modelling nonstrict effectful programs in the proof assistant Coq to formalise properties of such programs. We currently have a prototype compiler that transforms Haskell code into Coq using a representation based on free monads. The semantics correspond to callbyname. The general idea and basic transformation scheme is explained in the publication One Monad to Prove Them All, which is set in a fairytale theme. The succeeding publication Verifying Effectful Haskell Programs Using Coq sets the focus on more complex effects like error messages and tracing as well as advanced Haskell constructs like strict fields. A current topic for future work involves a representation that models callbyneed in order to prove properties about Haskell programs containing tracing effects, or Curry programs that entail nondeterminism as an effect.
Publications
 Verifying Effectful Haskell Programs in Coq

Implementing a Library for Probabilistic Programming using Nonstrict Nondeterminism
Journal on Theory and Practice of Logic Programming, July 2019
with Jan Christiansen, and Finn Teegen 
One Monad To Prove Them All
Journal on the Art, Science, and Engineering of Programming, Volume 3, 2019
with Jan Christiansen, and Finn Teegen 
Probabilistic Functional Logic Programming
International Symposium on Practical Aspects of Declarative Languages 2018 (acceptance ratio 13/23)
with Jan Christiansen, and Finn Teegen 
All Sorts of Permutations (Functional Pearl)
International Conference on Functional Programming 2016 (acceptance ratio 37/115)
with Jan Christiansen, and Nikita Danilenko