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