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. Have a look at my cv or this photo.

I study programming languages, type theories, and logics. I am particularly interested in applying semantic methods to prove syntactic properties of modal type theories and programming languages. I am also involved in the development of program logics for concurrent programming languages through the Iris project.

Carlo Angiuli and I are currently working on a book on dependent type theory. An early draft of the manuscript is available here: Principles of Dependent Type Theory.

Recent News

• 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