I am an assistant professor in the Department of Computer Science at Aarhus University in the Logic and Semantics group. 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 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

• New preprint: the Yoneda embedding in simplicial type theory.
• Idempotent resources in separation logic has been accepted to FoSSaCS 2025.
• 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.