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. see SMTCoq.
Publications
Students
- Michael Armand
- Sylvain Heraud
Former Student
Projects
- INRIA-Microsoft Research Joint Lab
- ANR Scalp : Security of Cryptographic ALgorithms with Probabilities
- ANR DeCert: Certified Decision procedures
Finished Projects
Contact
| E-mail: | Benjamin.Gregoire@sophia.inria.fr |
| Snail mail: | Projet Marelle, INRIA Sophia Antipolis, |
| 2004 route des Lucioles, B.P. 93, | |
| 06902 Sophia Antipolis Cedex | |
| Phone: | 04 92 38 75 59 (from France), +33 4 92 38 75 59 (from abroad) |
| Fax: | 04 92 38 50 29 (from France), +33 4 92 38 50 29 (from abroad) |