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

Je participe également à la conception et au développement de :

Publications

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

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

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

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

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

  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, avec Renaud Blanch, Jérémy Bluteau et Sabine Coquillart, ITS - ACM International Conference on Interactive Tabletops and Surfaces - 2012. BIBTEX

  8. Parametricity in an Impredicative Sort, avec 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, 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

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

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

  12. 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 23 novembre 2016