Welcome to my research page.

I am a post-doc in the Deducteam in the LMF (Laboratoire M├ęthodes Formelles), located in ENS Paris-Saclay (south of Paris), under the supervision of Chantal Keller and Valentin Blot.
I am in the development team of the Coq module Sniper, which help do some proof automation in Coq. Currently, Sniper is a part of the SMTCoq project.
I used to be a Phd student at IRIF (Paris) and a post-doc in the Gallinette Inria team (Nantes).
You may find here a short curriculum vitae.