A Verified Framework for Higher-Order Uncurrying Optimizations
to appear in Higher-Order and Symbolic Computation
with Xavier Leroy
paper

Vérification formelle d'un compilateur pour langages fonctionnels
Thèse, Université Paris 7 Diderot, July 2009.
document

Mechanized Verification of CPS transformations
Logic For Programming Artificial Intelligence and Reasoning 2007
with Xavier Leroy
paper

Décurryfication certifiée
Journées Francophones des Langages Applicatifs 2007
paper

Formal Verification of a C Compiler Front-End
with Sandrine Blazy and Xavier Leroy
Proceeding of Formal Methods 2006
paper