- Proving the equivalence of type and function definitions automatically in Coq
- Cut elimination in focusing with selection (M2)
- Automated CTL proofs in proof assistants (M1-M2)
- Combinaison des approches algébrique et "à la Hoare" : Preuve de concept (M2)
- Local extensions of type theory with new definitional equalities (M2)