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

Other developments

I also take part in the conception and the development of:

Publications

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

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

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

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

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

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

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

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

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

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

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

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

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: Nov. 23rd 2016