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