Français English


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

Other developments

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


Conferences and workshops with proceedings
  1. 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

  2. Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL, TAP - 12th International Conference on Tests and Proofs - 2018. PDF, BIBTEX

  3. 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

  4. 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

  5. A Certified Compiler for Verifiable Computing, with Cédric Fournet and Vincent Laporte, CSF - 29th IEEE Computer Security Foundations Symposium - 2016. PDF, BIBTEX

  6. 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

  7. 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

  8. Typeful Normalization by Evaluation, with Olivier Danvy and Matthias Puech, TYPES - 20th International Conference on Types for Proofs and Programs - 2014. PDF, BIBTEX

  9. 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

  10. Extended Resolution as Certificates for Propositional Logic, PxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013. PDF, BIBTEX

  11. 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

  12. Parametricity in an Impredicative Sort, with Marc Lasson, CSL - 26th International Workshop/21st Annual Conference of the EACSL - 2012. PDF, PS, BIBTEX

  13. 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

  14. 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

  15. Hereditary Substitutions for Simple Types, Formalized, with Thorsten Altenkirch, MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010. PDF, BIBTEX

  16. Importing HOL Light into Coq, with Benjamin Werner, ITP - Interactive Theorem Proving, First International Conference - 2010. PDF, BIBTEX

Conferences and workshops without proceedings
  1. 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
  1. SMTCoq : Mixing automatic and interactive proof technologies, book chapter of Proof Technology in Mathematics Research and Teaching, 2019.
Ph.D. thesis
  1. 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
  1. 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

  2. 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

  3. 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
  1. The category of simply typed λ-terms in Agda. PDF, BIBTEX

  2. A Matter of Trust: Skeptical Communication Between Coq and External Provers (Detailed Description). PDF

Home Research Teaching Studies Miscellaneous

Last update: Oct. 9th 2019