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 below).