Researchers

I am a researcher in the Marelle Team at Inria Sophia Antipolis. Most of my work deals with compilers, formal proofs, certification of cryptographic algorithms, proof assistants, type theory and proof by reflexion. I am one of the main implementers of CertiCrypt and EasyCrypt. I also participate to the development of native-coq a Coq version using the native Ocaml compiler to perform strong reduction. seeSMTCoq.