Français English
Research
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.
Publications
Conferences and workshops with proceedings
-
A Coq Formalization of Data Provenance, with Véronique Benzaken,
Sarah Cohen-Boulakia, Évelyne Contejean and Rébecca Zucchini,
CPP - 11th International
Conference on Certified Programs and Proofs -
2021. PDF.
-
On the Semantics of Polychronous Polytimed Specifications, with Hai
Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Benoît Valiron and Burkhart Wolff,
FORMATS - 18th International
Conference on Formal Modeling and Analysis of Timed Systems -
2020. PDF,
BIBTEX.
-
A Coq
formalisation of SQL's execution engines, with Véronique
Benzaken, Évelyne Contejean and Eunice Martins,
ITP - 9th International Conference on
Interactive Theorem Proving -
2018. PDF,
BIBTEX
-
Tactic
Program-Based Testing and Bounded Verification in Isabelle/HOL,
TAP - 12th International Conference on
Tests and Proofs -
2018. PDF,
BIBTEX
-
A Symbolic
Operational Semantics for TESL - With an Application to
Heterogeneous System Testing, with Hai Nguyen Van, Thibaut
Balabonski, Frédéric Boulanger, Benoît Valiron and Burkhart Wolff,
FORMATS - 15th International Conference on
Formal Modeling and Analysis of Timed Systems -
2017. PDF,
BIBTEX
-
SMTCoq: A
Plug-In for Integrating SMT Solvers into Coq, with Burak Ekici,
Alain Mebsout, Cesare Tinelli, Guy Katz, Andrew Reynolds and Clark W.
Barrett,
CAV - 29th
International Conference on Computer Aided Verification -
2017. PDF,
BIBTEX
-
A Certified
Compiler for Verifiable Computing, with Cédric Fournet
and Vincent Laporte,
CSF - 29th
IEEE Computer Security Foundations Symposium -
2016. PDF,
BIBTEX
-
Dependent types
and multi-monadic effects in F*, with Nikhil Swamy,
Catalin Hritcu, Aseem Rastogi, Antoine Delignat-Lavaud, Simon
Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub,
Markulf Kohlweiss, Jean Karim Zinzindohoue and Santiago Zanella
Béguelin,
POPL -
43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages - 2016. PDF,
BIBTEX
-
Extending
SMTCoq, a Certified Checker for SMT (Extended Abstract),
with Burak Ekici, Guy Katz, Alain Mebsout, Andrew J. Reynolds and
Cesare Tinelli,
HaTT -
1st International Workshop on Hammers for Type Theories -
2016. PDF,
BIBTEX
-
Typeful
Normalization by Evaluation, with Olivier Danvy and Matthias Puech,
TYPES -
20th International Conference on Types for Proofs and
Programs -
2014. PDF, BIBTEX
-
Beagle as a
HOL4 external ATP method, with Thibault Gauthier, Cezary
Kaliszyk and Michael Norrish,
PAAR - 4th Workshop on Practical Aspects of Automated Reasoning - 2014. PDF, BIBTEX
-
Extended Resolution as Certificates for Propositional Logic,
PxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013. PDF, BIBTEX
-
Pseudo-Weight: Making Tabletop Interaction with Virtual Objects More
Tangible, with Renaud Blanch, Jérémy Bluteau and Sabine Coquillart,
ITS - ACM International Conference
on Interactive Tabletops and Surfaces - 2012. BIBTEX
-
Parametricity
in an Impredicative Sort, with Marc Lasson,
CSL - 26th International
Workshop/21st Annual Conference of the EACSL -
2012. PDF,
PS, BIBTEX
-
A
Modular Integration of SAT/SMT Solvers to Coq through Proof
Witnesses, with Michaël Armand, Germain Faure, Benjamin
Grégoire, Laurent Théry and Benjamin Werner,
CPP - Certified Programs and Proofs
- First International Conference -
2011. PDF, BIBTEX
-
Verifying SAT and SMT in Coq for a fully automated decision procedure, with Michaël Armand, Germain Faure, Benjamin
Grégoire, Laurent Théry and Benjamin Werner
PSATTT - International Workshop on Proof-Search in Axiomatic
Theories and Type Theories - 2011. PDF, BIBTEX
-
Hereditary
Substitutions for Simple Types, Formalized, with Thorsten Altenkirch,
MSFP - Third Workshop on
Mathematically Structured Functional Programming -
2010. PDF, BIBTEX
-
Importing
HOL Light into Coq, with Benjamin Werner,
ITP -
Interactive Theorem Proving, First International Conference -
2010. PDF, BIBTEX
Conferences and workshops without proceedings
-
The
Refined Calculus of Inductive Construction: Parametricity and
Abstraction, with Marc Lasson,
LICS - 27th Annual
IEEE Symposium on Logic in Computer Science -
2012. PDF,
PS, BIBTEX
Book chapter
- SMTCoq :
Mixing automatic and interactive proof technologies, book chapter
of Proof
Technology in Mathematics Research and Teaching, 2019.
Ph.D. thesis
-
A Matter of Trust: Skeptical Communication Between Coq
and External Provers, PhD. thesis
at École Polytechnique
under the supervision of Benjamin
Werner and Germain Faure in the
Inria TypiCal
team of Laboratoire
d'Informatique de
Polytechnique - 2013. PDF, BIBTEX
Internship reports
-
Importation de
preuves HOL Light en Coq (in French), master internship under
the supervision of Benjamin
Werner in the
Inria TypiCal team
of Laboratoire
d'Informatique de
Polytechnique - 2009. PDF, BIBTEX
-
Substitutions for
simply-typed λ-calculus, master internship under the supervision
of Thorsten
Altenkirch in the Functional Programming team of the
School of Computer
Science at the
University of
Nottingham - 2008. PDF, BIBTEX
-
Manipulation
pseudo-haptique d'entités 2D (in French), licence internship
under the supervision
of Sabine
Coquillart and Renaud
Blanch at Inria
Rhône-Alpes and Laboratoire
d'Informatique de
Grenoble - 2007. PDF, BIBTEX
Unpublished notes
-
The
category of simply typed λ-terms in Agda. PDF, BIBTEX
-
A
Matter of Trust: Skeptical Communication Between Coq and External
Provers (Detailed Description). PDF
Last update: Dec. 24th 2020