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.