I am a postdoctoral researcher in the Department of Computer Science at Aarhus University under Lars Birkedal. I am presently at Oxford University as a visiting researcher and will start as an assistant professor at Aarhus University in the spring of 2025. Have a look at my cv or this photo.

I study programming languages and type theories through the lens of category theory. While I am broadly interested in these subjects, my research is focused on dependent type theory and more specifically on modal or homotopy type theory. For instance, I am interested in the following research topics:

• Applications of modal type theory to synthetic (∞,1)-category theory
• Using categorical methods to analyze different modal type theories
• Using guarded dependent type theories to study denotational semantics
• Using categorical logic to improve and refine program logics such as Iris

If you are interested in collaborating on these questions or if you are a student interested in pursuing an internship or Ph.D. with me, I encourage you to send me an email.

Forthcoming book

Carlo Angiuli and I are writing a book on dependent type theory. An early draft is available here: Principles of Dependent Type Theory. Please feel free to contact me if you find any errors (typographical or otherwise).

Recent News

• Unifying cubical and multimodal type theory has been accepted to LMCS
• New preprint: Idempotent resources in separation logic
• A modal deconstruction of Löb induction has been conditionally accepted.
• I’m visiting the University of Oxford from August 2024 to February 2025.
• New preprint: Directed univalence in simplicial homotopy type theory