I work on a Coq-checkable proof-trace system for SMT-solver Alt-Ergo.

Formerly, I was :

• Postdoc in project Tools for Proofs at INRIA-Microsoft research joint lab.
• PhD student in project Typical at Ecole Polytechnique.
• Member of ARC Corias.
• Moniteur at Université Paris Diderot.