Benjamin Grégoire
Inria Sophia Antipolis - Méditerranée

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.

+33 4 9238 7559
Publications at the Joint Centre:

Search Results –> Url version détaillée , Url version formatée
Criteria : Author : “benjamin,gregoire”
Number of occurrences founded : 42.