Research

My research is centered around formal program verification, program logics (e.g., Iris), and semantics of programming languages. I am also interested in type theory and category theory, particularly their applications to logic and programming languages. I use proof assistants, especially Rocq, extensively in my work, both as a tool for mechanizing mathematics, including programming languages theory and program verification approaches, and as a subject of study in their own right. See my publications for more details.

• 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.

• Léon Ducruet
• Ines Wright, co-advised with Lars Birkedal
• Arnaud Daby-Seesaram, co-advised with Lars Birkedal
• Anders Alnor Mathiasen, co-advised with Lars Birkedal
• Egor Namakonov, co-advised with Lars Birkedal

• Jonas Kastberg Hinrichsen

• Tobias Reinhard (KU Leuven), co-advised with Bart Jacobs — Dissertation: Lirias
• Abel Nieto Rodriguez, co-advised with Lars Birkedal — Dissertation: .pdf
• Simon Oddershede Gregersen, co-advised with Lars Birkedal — Dissertation: .pdf
• Koen Jacobs (KU Leuven), co-advised with Bart Jacobs & Dominique Devriese — Dissertation: Lirias

• Alban Reynaud, ENS Lyon (Aug 30 2021 — Jan 28, 2022)
• Paulo Emílio de Vilhena, Inria Paris (Jun 14 — Sep 14, 2021)