I am a full-time researcher at Inria.

I am based in Saclay, in the Toccata team, also part of the VALS team.

I am also involved in the DeepSea project at Inria Rocquencourt

My research interests span from programming languages to mechanized proofs.

Program verification
Formal metatheory in Coq
Multicore programming
Libraries for the Coq proof assistant