Français English

Recherche

Développements actuels

• Je participe à la conception et au développement de HOL-TestGen, un générateur de tests unitaires basé sur Isabelle/HOL. Je travaille notamment sur le back-end SMT pour la génération automatique de tests avec contraintes.
• Je participe à la conception et au développement de spécifications profondes pour les applications centrées données, au sein du projet DataCert. J'ai notamment formalisé la partie backend de la compilation de SQL.
• Je conçois et développe SMTCoq, une interface permettant à Coq de vérifier les réponses fournies par des prouveurs SAT et SMT externes, aussi bien pour la vérification a posteriori que pour de nouvelles tactiques automatiques dans Coq.

Autres développements

• PinocchioQ, un compilateur certifié pour Pinocchio, un protocole cryptographique pour le calcul vérifiable ("verifiable computing").
• F*, un langage de programmation à la ML avec des types plus expressifs, pour la preuve de programmes d'ordre supérieur avec effets (entrées/sorties, non terminaison, ...).
• ParamCoq, un générateur de "theorems for free" en Coq basé sur la théorie de la paramétricité ;
• HOLLIGHTCOQ, une interface permettant d'importer et de re-vérifier les théorèmes de HOL-Light en Coq.

Publications

1. A Coq Formalization of Data Provenance, avec Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean et Rébecca Zucchini, CPP - 11^th International Conference on Certified Programs and Proofs - 2021. PDF.


2. On the Semantics of Polychronous Polytimed Specifications, avec Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Benoît Valiron et Burkhart Wolff, FORMATS - 18^th International Conference on Formal Modeling and Analysis of Timed Systems - 2020. PDF, BIBTEX.


3. A Coq formalisation of SQL's execution engines, avec Véronique Benzaken, Évelyne Contejean et Eunice Martins, ITP - 9^th International Conference on Interactive Theorem Proving - 2018. PDF, BIBTEX


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


5. 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 - 15^th International Conference on Formal Modeling and Analysis of Timed Systems - 2017. PDF, BIBTEX


6. 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 - 29^th International Conference on Computer Aided Verification - 2017. PDF, BIBTEX


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


8. 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 - 43^rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - 2016. PDF, BIBTEX


9. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), avec Burak Ekici, Guy Katz, Alain Mebsout, Andrew J. Reynolds et Cesare Tinelli, HaTT - 1^st International Workshop on Hammers for Type Theories - 2016. PDF, BIBTEX


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


11. Beagle as a HOL4 external ATP method, avec Thibault Gauthier, Cezary Kaliszyk et Michael Norrish, PAAR - 4^th Workshop on Practical Aspects of Automated Reasoning - 2014. PDF, BIBTEX


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


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


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


15. 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 - First International Conference on Certified Programs and Proofs - 2011. PDF, BIBTEX


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


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


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

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

1. SMTCoq : Mixing automatic and interactive proof technologies, chapitre du livre Proof Technology in Mathematics Research and Teaching, 2019.

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

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

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

Dernière mise à jour le 24 décembre 2020