Français English

Recherche

Je m'intéresse à la théorie des langages de programmation et aux méthodes formelles, notamment au travers de la théorie des types, de la combinaison de prouveurs automatiques et interactifs, et de la preuve et du test de programmes. Je m'intéresse aux applications dans de nombreux domaines allant des langages de programmation eux-mêmes à la sécurité.

Développements actuels

Autres développements

Par le passé, j'ai participé à la conception et au développement de :

Publications

Communications avec actes
  1. A Coq formalisation of SQL's execution engines, avec Véronique Benzaken, Évelyne Contejean et 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, avec Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Benoît Valiron et 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, avec Burak Ekici, Alain Mebsout, Cesare Tinelli, Guy Katz, Andrew Reynolds et Clark W. Barrett, CAV - 29th International Conference on Computer Aided Verification - 2017. PDF, BIBTEX

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

  6. Dependent types and multi-monadic effects in F*, avec Nikhil Swamy, Catalin Hritcu, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue et 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), avec Burak Ekici, Guy Katz, Alain Mebsout, Andrew J. Reynolds et Cesare Tinelli, HaTT - 1st International Workshop on Hammers for Type Theories - 2016. PDF, BIBTEX

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

  9. Beagle as a HOL4 external ATP method, avec Thibault Gauthier, Cezary Kaliszyk et 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, avec Renaud Blanch, Jérémy Bluteau et Sabine Coquillart, ITS - ACM International Conference on Interactive Tabletops and Surfaces - 2012. BIBTEX

  12. Parametricity in an Impredicative Sort, avec 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, avec Michaël Armand, Germain Faure, Benjamin Grégoire, Laurent Théry et 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, avec Michaël Armand, Germain Faure, Benjamin Grégoire, Laurent Théry et Benjamin Werner, PSATTT - International Workshop on Proof-Search in Axiomatic Theories and Type Theories - 2011. PDF, BIBTEX

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

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

Communications sans actes
  1. The Refined Calculus of Inductive Construction: Parametricity and Abstraction, avec Marc Lasson, LICS - 27th Annual IEEE Symposium on Logic in Computer Science - 2012. PDF, PS, BIBTEX

Thèse de doctorat
  1. A Matter of Trust: Skeptical Communication Between Coq and External Provers, thèse de l'École Polytechnique sous la direction de Benjamin Werner et Germain Faure dans l'équipe Inria TypiCal du Laboratoire d'Informatique de Polytechnique - 2013. PDF, BIBTEX

Rapports de stages
  1. Importation de preuves HOL Light en Coq, rapport de stage de Master sous la direction de Benjamin Werner dans l'équipe Inria TypiCal du Laboratoire d'Informatique de Polytechnique - 2009. PDF, BIBTEX

  2. Substitutions for simply-typed λ-calculus, rapport de stage de Master sous la direction de Thorsten Altenkirch dans l'équipe Functional Programming de la School of Computer Science de l'Université de Nottingham - 2008. PDF, BIBTEX

  3. Manipulation pseudo-haptique d'entités 2D, rapport de stage de Licence sous la direction de Sabine Coquillart et Renaud Blanch à l'Inria Rhône-Alpes et au Laboratoire d'Informatique de Grenoble - 2007. PDF, BIBTEX

Documents non publiés
  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


Accueil Recherche Enseignement Études Divers

Dernière mise à jour le 1er octobre 2018