My research is focused on formal program verification, program logics (e.g., Iris), semantics of programs and programming languages, compilers, type theory, proof assistants (e.g., Coq), and formalization of mathematical proofs, especially theory of programming languages in proof assistants. More generally, I am also interested in Category theory, especially for its application to logic and programming languages semantics, formal logic, and foundations of mathematics. See my publications for more details.
Past research projects:
- Postdoctoral fellowship of Flemish research fund (FWO) for studying programming languages with advanced features in program logics.
- KU Leuven internal funding project for relational reasoning about advanced type systems.
- Anders Alnor Mathiasen, co-advised with Lars Birkedal
- Egor Namakonov, co-advised with Lars Birkedal
- Abel Nieto, co-advised with Lars Birkedal
- Tobias Reinhard (KU Leuven), co-advised with Bart Jacobs
Past PhD Students:
- Simon Oddershede Gregersen, co-advised with Lars Birkedal (Continued as a postdoc in LogSem)
- Koen Jacobs (KU Leuven), co-advised with Bart Jacobs (Now postdoc at Inria with Éric Tanter & Nicolas Tabareau)
- Paulo Emílio de Vilhena, Inria Paris (Jun 14 — Sep 14, 2021)