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.

• I am the coordinator of the Digicosme UPSCaLe working group, joint between LIX, LMF, LSV, Samovar, U2IS, and Inria Saclay - Île-de-France.
• In 2021, I am a member of the ITP and TAP program committees, vice-chair of JFLA, and co-chair of PxTP.
• In 2020, I was a member of the JFLA, TAP, and SMT program committees.
• In 2019, I was a member of the CPP, Coq workshop, TyDe and PxTP program committees, and I am PC chair of TAP.
• In 2018, I was a member of the ITP, LFMTP, CoqPL, OBT, PAAR and TAP program committees.
• In 2017, I was a member of the POPL external program committee and the PxTP program committee.
• In 2016, I was a member of the MSFP, PAAR, LFMTP and HATT program committees.

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.