I am a Senior Haskell Developer at Wire.

Until February 2021, I was a postdoc at the Logic Group in TU Darmstadt, working on homotopy type theory and category theory. Previously, I was a postdoc at the University of Nottingham, where I also got my PhD under the supervision of Venanzio Capretta.

Publications

Two-Level Type Theory and Applications [bibtex]

With Danil Annenkov, Nicolai Kraus and Christian Sattler.
Published in MSCS.
Formalisation.

Higher lenses [bibtex]

With Nils Anders Danielsson and Andrea Vezzosi. Proceedings of LICS 2021.

Quotient inductive-inductive types [bibtex]

With Thorsten Altenkirch, Gabe Dijkstra, Nicolai Kraus and Fredrik Nordvall Forsberg.
Proceedings of FoSSaCS 2018.
Semantics for certain classes of higher inductive definitions in 0-truncated Homotopy Type Theory.

Univalent higher categories via complete semi-Segal types [bibtex]

With Nicolai Kraus.
Proceedings of POPL 2018.
Formalisation.

Models of type theory with strict equality [bibtex]

My PhD thesis.

Extending Homotopy Type Theory with strict equality [bibtex]

With Thorsten Altenkirch and Nicolai Kraus.
Proceedings of CSL 2016

Functions out of higher truncations [bibtex]

With Nicolai Kraus and Andrea Vezzosi.
Proceedings of CSL 2015.

Non-wellfounded trees in Homotopy Type Theory [bibtex]

With Benedikt Ahrens and Régis Spadotti.
Proceedings of TLCA 2015, LIPIcs Vol. 38, pp. 17-30.
Project webpage.

Free applicative functors [bibtex]

With Ambrus Kaposi.
Proceedings of MSFP 2014.
Previous version, submitted to ICFP 2013.

Recent work

Lecture notes on topology

Lecture notes for an introductory topology course given at TU Darmstadt in the Summer semester of 2019.

Lecture notes on semantics of type theory

An introduction to models of type theory and the construction of the simplicial model, based on a course given at TU Darmstadt in the Summer semester of 2020.

Mutual and Higher Inductive Types in Homotopy Type Theory

My paper for the FP Lab Away Day 2014. An internalisation of the syntax of mutual and higher inductive types in 0-truncated Homotopy Type Theory.

Inheritance and overloading in Agda

My paper for the FP Lab Away Day 2013 (slides). An exposition of the techniques I used in the implementation of my category theory library in Agda.

Type theory through comprehension categories

My first year report: an introduction to fibrational models of type theory.

Projects

agda-categories

An implementation of basic category theory in Agda/HoTT.

agda-base

Base library for homotopy type theory in Agda.

optparse-applicative

A Haskell library for parsing command line options using Applicative functors.

Contact