I am a full-time researcher at Inria Saclay, in the Toccata team.
I am also involved in a project at Inria Rocquencourt, with Umut Acar and Mike Rainey.

My research interests span from programming languages to formal proofs.

Program verification
Formal metatheory in Coq
Classical libraries for Coq
Multicore programming