My research primarly focuses on improving interactive theorem provers (ITPs), and
the application of ITPs to the verification of proofs. Here is a non-exhaustive list of topics:
At the moment, I'm currently working in a new typed language for tactic
programming, and a new unification algorithm for the Coq proof assistant (check my list of publications
- Proof automation.
- Typed tactics.
- Unification and elaboration algorithms.
- Type theories.
- Verification of logics.
- Verification of programming languages.