I joined the Institute for Programming Languages and Systems in September 2026. Before that I finished my MSc in mathematics at Stockholm University, jointly with KTH Royal Institute of Technology, in February 2026. My thesis, The Category of Iterative Sets in Cubical Agda, was supervised by Anders Mörtberg and awarded the Mittag-Leffler Prize.
My bachelor’s degrees, in mathematics and in computer science, are from LMU Munich, where I also taught exercise classes for three semesters on logic, formal languages and complexity. From 2023 to 2026 I organised the Stockholm Master in Mathematics Seminar, a student-led seminar for mathematics master’s students.
I also enjoy recreational programming. I particularly like working with Haskell and Rust, as they allow me to write safe and efficient programs with ease.
-
The Category of Iterative Sets in Cubical Agda
Master’s thesis, Mathematics M.Sc., Stockholm University, 2026
Talks on it: Stockholm–Gothenburg Type Theory Meeting (); Master’s thesis defence, Stockholm University ()
-
A Gentle Introduction to Homotopy Type Theory
Talk, 16 September 2025, Stockholm Master in Mathematics Seminar
-
A Predicative Approach to the Constructive Integration Theory of Locally Compact Metric Spaces
Article, 2025, with Iosif Petrakis, Journal of Logic and Analysis, volume 17
-
linlog
A linear logic prover and educational tool
Project in Rust
-
Determinize
A probabilistic language with E/G sampling modes, implemented and formalised in Lean, with exact expected-reward certificates and a browser simulator.
Contribution in Lean, with Jules Jacobs, Katherine Wu, Kevin Batz & Alexandra Silva
More under Publications, Talks and Projects.
Write to me in English or in German. My postal address and my OpenPGP keys are on the contact page.
