(This vitae is also available in english.)

Xavier Leroy

État-civil

Né le 15 mars 1968. Nationalité française.

Thèmes de recherche

Conception, implémentation, formalisation et vérification formelle des langages et outils de programmation.
En particulier:

Cursus universitaire

Activités de recherche

Depuis 2006
Directeur de recherche, INRIA Paris-Rocquencourt, projet Gallium. (Responsable scientifique du projet.)
2000 - 2005
Directeur de recherche, INRIA Rocquencourt, projet Cristal. (Responsable scientifique du projet depuis 2003.)
1994 - 2000
Chargé de recherche, INRIA Rocquencourt, projet Cristal.
1993 - 1994
Post-doc, université Stanford (Californie), dans le groupe de John Mitchell.
1989 - 1992
Doctorant, ENS et INRIA Rocquencourt, projet Formel, sous la direction de Gérard Huet.
Été 1989
Stagiaire, DEC Systems Research Center, sous la direction de Luca Cardelli.

Activités dans l'industrie

1999-2004
Ingénieur puis consultant pour Trusted Logic, une start-up dans le domaine des cartes à puces et autres systèmes embarqués sécuritaires.
1997 - 1998
Consultant pour Bull CP8 sur JavaCard (Java sur cartes à puces).

Activités d'enseignement

2006-2008 et 2010-maintenant
Enseignant au Master MPRI (université Paris 7, ENS Paris, ENS Cachan, Polytechnique). (Langages fonctionnels, sémantiques opérationnelles, compilation.)
1995-2001
Enseignant au DEA Programmation: Sémantique, Preuve et Langages (universités Paris 6, 7, Sud; ENS Paris; Polytechnique). (1995-1997: compilation avancée; 1998-2001: systèmes de types).
1991-1992
Assistant moniteur normalien à l'École Normale Supérieure.

Principales publications

Livres:

  1. Le langage Caml, avec Pierre Weis. Seconde édition Dunod, Paris, 1999; première édition InterÉditions, Paris, 1993.
  2. Manuel de référence du langage Caml, avec Pierre Weis. InterÉditions, Paris, 1993.

Articles de revues et chapitres de livres:

  1. Verified compilation of floating-point computation, avec Sylvie Boldo, Jacques-Henri Jourdan, et Guillaume Melquiond.
    Journal of Automated Reasoning 54(2), 2015.
  2. The CompCert memory model, avec Andrew W. Appel, Sandrine Blazy, and Gordon Stewart.
    In Program Logics for Certified Compilers, pages 237-271. Cambridge University Press, mars 2014.
  3. A list-machine benchmark for mechanized metatheory, avec Andrew W. Appel et Robert Dockins.
    Journal of Automated Reasoning 49(3), 2012.
  4. Formal verification of a realistic compiler.
    Communications of the ACM 52(7), 2009.
  5. A verified framework for higher-order uncurrying optimizations, avec Zaynah Dargaye.
    Higher-Order and Symbolic Computation 22(3), 2009.
  6. Mechanized semantics for the Clight subset of the C language, avec Sandrine Blazy.
    Journal of Automated Reasoning 43(3), 2009.
  7. Compilation of extended recursion in call-by-value functional languages, avec Tom Hirschowitz et J. B. Wells.
    Higher-Order and Symbolic Computation 22(1), 2009.
  8. Coinductive big-step operational semantics, avec Hervé Grall.
    Information and Computation 207(2):284-304, 2009.
  9. Formal verification of a C-like memory model and its uses for verifying program transformations, avec Sandrine Blazy.
    Journal of Automated Reasoning 41(1), 2008.
  10. Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves, avec Laurence Rideau et Bernard P. Serpette.
    Journal of Automated Reasoning 40(4), 2008.
  11. Mixin modules in a call-by-value setting, avec Tom Hirschowitz.
    ACM Transactions on Programming Languages and Systems, 27(5), 2005.
  12. Java bytecode verification: algorithms and formalizations.
    Journal of Automated Reasoning 30(3-4), 2003.
  13. Bytecode verification for Java smart card.
    Software Practice & Experience 32, 2002.
  14. Type-based analysis of uncaught exceptions, avec François Pessaux.
    ACM Transactions on Programming Languages and Systems 22(2), 2000.
  15. A modular module system.
    Journal of Functional Programming 10(3), 2000.
  16. Security properties of typed applets, avec François Rouaix.
    In Secure Internet Programming: Issues in Distributed and Mobile Object Systems, LNCS 1603, Springer-Verlag, 1999.
  17. A syntactic theory of type generativity and sharing.
    Journal of Functional Programming, 6(5), 1996.
  18. Dynamics in ML, avec Michel Mauny.
    Journal of Functional Programming 3(4), 1993.

Articles dans des congrès avec comité de lecture:

  1. A formally-verified C static analyzer, avec Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, et David Pichardie.
    Principles of Programming Languages (POPL 2015), janvier 2015.
  2. Formal C semantics: CompCert and the C standard, avec Robbert Krebbers et Freek Wiedijk.
    Interactive Theorem Proving (ITP 2014), juillet 2014.
  3. A formally-verified C compiler supporting floating-point arithmetic, avec Sylvie Boldo, Jacques-Henri Jourdan, et Guillaume Melquiond.
    21st IEEE symposium on Computer Arithmetic, ARITH 21, avril 2013.
  4. Validating LR(1) parsers, avec Jacques-Henri Jourdan and François Pottier.
    European Symposium on Programming (ESOP 2012), avril 2012.
  5. Formally verified optimizing compilation in ACG-based flight control software, avec Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Marc Pantel et Jean Souyris.
    Embedded Real Time Software and Systems (ERTS 2012), février 2012.
  6. A mechanized semantics for C++ object construction and destruction, with applications to resource management, avec Tahina Ramananandro et Gabriel Dos Reis.
    Principles of Programming Languages (POPL 2012), janvier 2012.
  7. Formal verification of object layout for C++ multiple inheritance, avec Tahina Ramananandro et Gabriel Dos Reis.
    Principles of Programming Languages (POPL 2011), janvier 2011.
  8. Validating register allocation and spilling, avec Silvain Rideau.
    Compiler Construction (CC 2010), mars 2010.
  9. A simple, verified validator for software pipelining, avec Jean-Baptiste Tristan.
    Principles of Programming Languages (POPL 2010), janvier 2010.
  10. Verified validation of Lazy Code Motion, avec Jean-Baptiste Tristan.
    Programming Languages Design and Implementation (PLDI 2009), juin 2009.
  11. Formal verification of translation validators: A case study on instruction scheduling optimizations, avec Jean-Baptiste Tristan.
    Principles of Programming Languages (POPL 2008), janvier 2008.
  12. Mechanized verification of CPS transformations, avec Zaynah Dargaye.
    Logic for Programming Artificial Intelligence and Reasoning (LPAR 2007), octobre 2007.
  13. Managing the complexity of large free and open source package-based software distributions, avec Fabio Mancinelli, Roberto Di Cosmo, Jérôme Vouillon, Jaap Boender, Berke Durak et Ralf Treinen.
    Automated Software Engineering (ASE 2006), septembre 2006.
  14. Formal verification of a C compiler front-end, avec Sandrine Blazy and Zaynah Dargaye.
    Formal Methods 2006, août 2006.
  15. A list-machine benchmark for mechanized metatheory, avec Andrew Appel.
    Workshop on Logical Frameworks and Meta-Languages, août 2006.
  16. Coinductive big-step operational semantics.
    European Symposium on Programming, mars 2006.
  17. Maintaining large software distributions: new challenges from the FOSS era, avec Roberto Di Cosmo, Berke Durak, Fabio Mancinelli et Jérôme Vouillon.
    Workshop FRCSS 2006, mars 2006.
  18. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant.
    Principles of Programming Languages, janvier 2006.
  19. Formal verification of a memory model for C-like imperative languages, avec Sandrine Blazy.
    International Conference on Formal Engineering Methods, novembre 2005.
  20. A structured approach to proving compiler optimizations based on dataflow analysis, avec Yves Bertot et Benjamin Grégoire.
    Post-workshop proceedings of TYPES 2004.
  21. Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types, avec Tom Hirschowitz et J.B.Wells.
    European Symposium on Programming 2004.
  22. Compilation of extended recursion in call-by-value functional languages, avec Tom Hirschowitz et J. B. Wells,
    Principles and Practice of Declarative Programming 2003.
  23. A compiled implementation of strong reduction, avec Benjamin Grégoire,
    International Conference on Functional Programming 2002.
  24. Mixin modules in a call-by-value setting, avec Tom Hirschowitz,
    European Symposium on Programming 2002.
  25. On-card bytecode verification for Java card,
    congrès e-Smart, septembre 2001.
  26. Type-based analysis of uncaught exceptions, avec François Pessaux,
    Principles of Programming Languages, janvier 1999.
  27. Security properties of typed applets, avec François Rouaix,
    Principles of Programming Languages, janvier 1998.
  28. The effectiveness of type-based unboxing,
    Workshop Types in Compilation '97, june 1997.
  29. Le système Caml Special Light: modules et compilation efficace en Caml,
    Journées Francophones des Langages Applicatifs, janvier 1996.
  30. Applicative functors and fully transparent higher-order modules,
    Principles of Programming Languages, janvier 1995.
  31. Manifest types, modules, and separate compilation,
    Principles of Programming Languages, janvier 1994.
  32. Polymorphism by name for references and continuations,
    Principles of Programming Languages, janvier 1993.
  33. A concurrent, generational garbage collector for a multithreaded implementation of ML, avec Damien Doligez,
    Principles of Programming Languages, janvier 1993.
  34. Unboxed objects and polymorphic typing,
    Principles of Programming Languages, janvier 1992.
  35. Dynamics in ML, avec Michel Mauny,
    Functional Programming and Computer Architecture, août 1991.
  36. Polymorphic type inference and assignment, avec Pierre Weis,
    Principles of Programming Languages, janvier 1991.
  37. Efficient data representation in polymorphic languages,
    Programming Language Implementation and Logic Programming, août 1990.
  38. Abstract types and the dot notation, avec Luca Cardelli,
    IFIP TC2 working conference on programming concepts and methods, avril 1990.

Autres publications:

  1. Introduction to Types in Compilation, actes du Workshop Types in Compilation, 1998.
  2. Typage polymorphe d'un langage algorithmique, thèse de doctorat, université Paris 7, 1992. Traduction anglaise: Polymorphic typing of an algorithmic language, rapport de recherche 1778, INRIA, 1992.
  3. The ZINC experiment: an economical implementation of the ML language. Rapport technique 117, INRIA, 1990.

Exposés invités et tutoriels:

  1. Compiler verification for fun and profit exposé invité, congrès FMCAD 2014.
  2. Formal proofs of code generation and verification tools, exposé invité, congrès SEFM 2014.
  3. Proof assistants in computer science research, exposé inaugural, trimestre thématique IHP sur Semantics of proofs and certified mathematics, Avril 2014.
  4. Mechanized semantics for compiler verification, exposé invité, congrès APLAS et CPP 2012.
  5. Mechanized verification of program transformations and static analyses, école d'été Oregon Programming Languages, 2010, 2011, 2012.
  6. Verified squared: does critical software deserve verified tools?, exposé invité, congrès POPL 2011.
  7. Mechanized semantics, cours à l'école Marktoberdorf 2009.
  8. Du langage à l'action: compilation et typage, intervention dans le cours de Gérard Berry au Collège de France en 2008.
  9. Formal verification of an optimizing compiler, exposé invité, congrès RTA 2007, MEMOCODE 2007, LCTES 2008.
  10. From Krivine's machine to the Caml implementations, exposé invité, KAZAM workshop, 2005.
  11. A unified framework for bytecode verification algorithms, exposé invité, Bytecode workshop, 2005.
  12. Language-based security for mobile code, with applications to smart cards, cours de 7 heures à TECS Week 2005.
  13. Exploiting type systems and static analyses for smart card security, exposé invité, CASSIS, mars 2004.
  14. Computer security from a programming language and static analysis perspective, exposé invité, ETAPS, avril 2003.
  15. Java bytecode verification: an overview, exposé invité, Computer Aided Verification, juillet 2001.
  16. Objects and classes vs. modules in Objective Caml, exposé invité, International Conference on Functional Programming, septembre 1999.
  17. Security properties of typed applets, exposé invité, APPIA-GULP-PRODE workshop on declarative programming, juillet 1998.
  18. Compilation techniques for functional and object-oriented languages, tutoriel, Programming Language Design and Implementation '98, juin 1998.
  19. An introduction to compiling functional languages, tutoriel, Workshop on Types in Compilation '98, mars 1998.

Développement de logiciels

Auteur du compilateur vérifié CompCert C pour logiciels embarqués critiques. CompCert C est le premier compilateur réaliste qui a été formellement vérifié à l'aide de méthodes formelles (l'assistant de preuves Coq).

Principal architecte et implémenteur du système OCaml, un dialecte du langage ML qui intègre un puissant système d'objets et de classes, un riche langage de modules, une machine virtuelle légère, portable et efficace, et un compilateur optimisant produisant du code machine très rapide. OCaml est utilisé dans les services de R&D de plusieurs grandes entreprises (IBM, Microsoft, Dassault), ainsi que dans plusieurs projets universitaires importants tels que Ensemble (Cornell) et Unison (U.Penn.).

Une implémentation antérieure et plus légère de Caml, appelée Caml Light, diffusée depuis 1991, est utilisée pour l'enseignement par plusieurs universités françaises et dans le cadre de l'option Informatique des classes préparatoires scientifiques.

Auteur de la bibliothèque LinuxThreads, une implémentation de la norme POSIX 1003.1c pour la programmation parallèle. De 1998 à 2004, LinuxThreads a été la bibliothèque de "threads" standard dans les distributions de Linux.

Auteur de plusieurs composants logiciels pour JavaCard (cartes à puces Java), en particulier une machine virtuelle JavaCard hautes performances, intégrée dans la carte Odyssey 1 de Bull CP8, et le premier vérificateur embarqué de code JavaCard, commercialisé par Axalto sous le nom Codeshield.

Prix et distinctions

Prix Royal Society Milner Award 2016.

Fellow of the ACM (depuis 2015).

Prix Microsoft Research Verified Software Milestone Award 2012.

Prix La Recherche 2011 en sciences de l'information, avec Sandrine Blazy, Zaynah Dargaye et Jean-Baptiste Tristan.

Prix Michel Monpetit 2007 de l'Académie des Sciences.

ACM SIGPLAN Most Influential POPL Paper Award (pour mon article à POPL 2006).

Direction de thèses

  1. Directeur de thèse de Jacques-Henri Jourdan (depuis 2012).
  2. Directeur de thèse de Tahina Ramananandro (2007-2011). Tahina est actuellement ingénieur R&D chez Reservoir Labs, New York.
  3. Directeur de thèse de Jean-Baptiste Tristan (2006-2009). Jean-Baptiste est actuellement chercheur à Oracle Labs.
  4. Directeur de thèse de Zaynah Dargaye (2005-2009). Zaynah est actuellement ingénieur de recherche au CEA, laboratoire LIST.
  5. Directeur de thèse de Tom Hirschowitz (2000-2003). Tom est actuellement chargé de recherche au CNRS.
  6. Co-directeur de thèse (avec Benjamin Werner) de Benjamin Grégoire (1999-2003). Benjamin est actuellement chargé de recherche à l'INRIA.
  7. Directeur de thèse de François Pessaux (1997-1999). François est actuellement enseignant-chercheur à l'ENSTA ParisTech.

Responsabilités éditoriales

Membre du comité de rédaction de la revue Journal of the ACM.

Membre du comité de rédaction du mensuel Communications of the ACM, section Research Highlights.

Membre du comité de rédaction de la revue Journal of Automated Reasoning.

Participation à des comités de sélection

Président du comité de sélection des congrès POPL 2004 et ICFP 2001, et du workshop TIC 1998. Co-président du comité de sélection du congrès CPP 2015.

Membre des comités de sélection de Compiler Construction 2016, SNAPL 2015, ESOP 2013, POPL 2013, Compiler Construction 2011, PADL 2011, CPP 2011, VSTTE 2010, ITP 2010, ESOP 2009, ICFP 2009, TPHOLs 2009, CUFP 2007, ASIAN 2006, FM 2006, ML Workshop 2005, VEE 2005, ESOP 2005, CARDIS 2004, POPL 2004, FOOL 2003, JFLA 2003, CARDIS 2002, POPL 2002, ICFP 2001, Compiler Construction 2001, ICFP 2000, PLDI 2000, ESOP 2000, PPDP 1999, PLILP 1998, POPL 1998, TIC 1998, ICFP 1997, TIC 1997, FPCA 1995, and SAS 1994.

Membre du comité scientifique du programme SESUR 2007 de l'ANR.

Brevets

  1. Management protocol, method for verifying and transforming a downloaded programme fragment and corresponding systems / Protocole de gestion, procédé de verification et de transformation d'un fragment de programme téléchargé et systèmes correspondants, Trusted Logic, WO0114958, EP1212678, FR2797963.
  2. Control of data access by dynamically verifying legal references / Contrôle d'accès aux données par vérification dynamique des références licites, avec P. Hameau, N. Regnault, R. Marlet, Trusted Logic, WO2005073827, FR2864658.
  3. Method for controlling program execution integrity by verifying execution trace prints / Procédé de contrôle d'intégrité de programmes par vérification d'empreintes de traces d'exécution, avec D. Bolignano, R. Marlet, Trusted Logic, WO2005073859, EP1702268, FR2864655.

Divers


Page personnelle: http://gallium.inria.fr/~xleroy/