I am a member of the Laboratory of Formal Methods, teaching at the Computer Science Department at IUT d’Orsay. I am interested in programming languages and formal methods, notably through Type Theory, the combination of automated and interactive provers, and proof and test of programs. I apply these methods to many domains from programming languages themselves to security.

Current research developments

  • I am an active member of the development team of HOL-TestGen, a test case generator for specification based unit testing built on top of Isabelle/HOL. In particular, I am now working on the SMT back-end for automatic constrained test generation.
  • I am an active developer of deep specifications for data-centric applications, in the DataCert project. In particular, I formalized the SQL compilation backend.
  • I am the main developer of SMTCoq, a Coq verifier for SAT and SMT proof witnesses, designed for /a posteriori/ verification as well as new automatic tactics in Coq.

Other developments

In the past, I took part in the conception and the development of:

  • PinocchioQ, a certified compiler for Pinocchio, a cryptographic protocol for verifiable computing.
  • F*, a programming language /à la ML/ with more expressive types, designed for the verification of higher-order, effectful programs (IO, non termination…).
  • ParamCoq, a “theorems for free” generator in Coq based on parametricity;
  • HOLLIGHTCOQ, an interface to import and re-check HOL-Light’s theorems in Coq.