(CV également disponible en version française.)

Xavier Leroy

Born March 15th, 1968. French citizen.

Research interests

Design, implementation, formalisation and formal verification of programming languages and tools.
In particular:

Education

Research experience

2006 - now
Senior research scientist (directeur de recherche), INRIA Rocquencourt, project-team Gallium. (Team leader.)
2000 - 2005
Senior research scientist (directeur de recherche), INRIA Rocquencourt, project-team Cristal. (Team leader since 2003.)
1994 - 2000
Junior research scientist (chargé de recherche), INRIA Rocquencourt, project-team Cristal.
1993 - 1994
Post-doc, Stanford University, in John Mitchell's group.
1989 - 1992
PhD student, ENS and INRIA Rocquencourt, project-team Formel, under Gérard Huet's supervision.
Summer 1989
Summer intern, DEC Systems Research Center, under Luca Cardelli's supervision.

Industrial experience

1999-2004
Engineer, then consultant, for Trusted Logic, a start-up working on smart cards and other secure embedded systems.
1997-1998
Consultant for Bull CP8 on JavaCard (Java on smartcarts).

Teaching experience

2006-2008 and 2010-now
Teaches a graduate course (functional programming, operational semantics, compilation) at the MPRI Master, a joint graduate curriculum of university Paris 7, ENS Paris, ENS Cachan and Polytechnique.
1995-2001
Teaches a graduate course (1995-1997: advanced compilation; 1998-2001: type systems) at the DEA Programmation (Sémantique, Preuve et Langages), a joint graduate curriculum of universities Paris 6, Paris 7, Paris 11, ENS Paris, and Polytechnique.
1991-1992
Teaching assistant (assistant moniteur normalien), École Normale Supérieure.

Selected publications

Books:

  1. Le langage Caml, with Pierre Weis. Second edition Dunod, Paris, 1999, first edition InterÉditions, Paris, 1993.
  2. Manuel de référence du langage Caml, with Pierre Weis. InterÉditions, Paris, 1993.

Journal articles and book chapters:

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

Papers in refereed conferences:

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

Other publications:

  1. Introduction to Types in Compilation, proceedings workshop Types in Compilation, 1998.
  2. Typage polymorphe d'un langage algorithmique, PhD dissertation, university Paris 7, 1992. English translation: Polymorphic typing of an algorithmic language, INRIA research report 1778, 1992.
  3. The ZINC experiment: an economical implementation of the ML language. INRIA technical report 117, 1990.

Invited lectures and tutorials:

  1. Mechanized semantics for compiler verification, invited lecture, APLAS and CPP 2012 joint conferences.
  2. Mechanized verification of program transformations and static analyses, Oregon Programming Languages summer school, 2010, 2011, 2012.
  3. Verified squared: does critical software deserve verified tools?, invited lecture, POPL 2011 conference.
  4. Mechanized semantics, lecture at the Marktoberdorf 2009 summer school.
  5. Du langage à l'action: compilation et typage, guest lecture in Gérard Berry's course at Collège de France, 2008.
  6. Formal verification of an optimizing compiler, invited lecture, conferences RTA 2007, MEMOCODE 2007, LCTES 2008.
  7. From Krivine's machine to the Caml implementations, invited lecture, KAZAM workshop, 2005.
  8. A unified framework for bytecode verification algorithms, invited lecture, Bytecode workshop, 2005.
  9. Language-based security for mobile code, with applications to smart cards, 7-hour lecture given at TECS Week 2005.
  10. Exploiting type systems and static analyses for smart card security, invited lecture, CASSIS, march 2004.
  11. Computer security from a programming language and static analysis perspective, invited lecture, ETAPS, april 2003.
  12. Java bytecode verification: an overview, invited lecture, Computer Aided Verification, july 2001.
  13. Objects and classes vs. modules in Objective Caml, invited lecture, International Conference on Functional Programming, sept 1999.
  14. Security properties of typed applets, invited lecture, APPIA-GULP-PRODE workshop on declarative programming, july 1998.
  15. Compilation techniques for functional and object-oriented languages, tutorial given at Programming Language Design and Implementation '98, june 1998.
  16. An introduction to compiling functional languages, tutorial given at the workshop on Types in Compilation '98, march 1998.

Software development

Author of the CompCert C verified compiler for critical embedded systems. CompCert C is the first realistic compiler that was formally verified using formal methods (the Coq proof assistant.)

Main architect and implementor of the Objective Caml, a portable and efficient implementation of the (Ca)ML language, featuring a complete class-based object-oriented system, state-of-the-art modules, and a high-performance native-code compiler. Objective Caml is used in the R&D departments of several large companies (IBM, Microsoft, Dassault), as well as in several advanced academic projects such as Ensemble (Cornell) and Unison (U.Penn.).

An earlier and smaller implementation of Caml, called Caml Light, publicly released since 1991, is used in undergraduate and graduate courses in several French universities and was selected as teaching language by the French Ministry of Education for the minor in computer science of the classes préparatoires scientifiques.

Author of the LinuxThreads library, an implementation of the POSIX 1003.1c threads interface for Linux that was the standard threads library for Linux distributions between 1998 and 2004.

Developed several software components for JavaCard (Java-enabled smart cards), including a high-performance JavaCard virtual machine, which is at the heart of Bull CP8's Odyssey 1 smart card, and the world's first on-card bytecode verifier for JavaCard, marketed by Axalto under the name Codeshield.

Awards

Recipient of the 2012 Microsoft Research Verified Software Milestone Award.

Recipient of the 2011 La Recherche prize in Information Sciences, jointly with Sandrine Blazy, Zaynah Dargaye and Jean-Baptiste Tristan.

Recipient of the Michel Monpetit 2007 award of the French Academy of Sciences.

PhD supervision

  1. PhD advisor for Jacques-Henri Jourdan (since 2012).
  2. PhD advisor for Tahina Ramananandro (2007-2011). Tahina is currently post-doc at Yale University.
  3. PhD advisor for Jean-Baptiste Tristan (2006-2009). Jean-Baptiste is currently research scientist at Oracle Labs.
  4. PhD advisor for Zaynah Dargaye (2005-2009). Zaynah is currently research engineer at CEA, LIST laboratory.
  5. PhD advisor for Tom Hirschowitz (2000-2003). Tom is currently research scientist at CNRS.
  6. PhD co-advisor (with Benjamin Werner) for Benjamin Grégoire (1999-2003). Benjamin is currently research scientist at INRIA.
  7. PhD advisor for François Pessaux (1997-1999). François is currently assistant professor at ENSTA ParisTech.

Editorship

Member of the editorial committee of Journal of Automated Reasoning.

Member of the editorial committee of Journal of Formalized Reasoning.

Program committees

Chairman of the program committees for POPL 2004, ICFP 2001 and TIC 1998.

Member of the program committees for 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.

Member of the scientific board of the «Computer Security and Safety» SESUR 2007 programme of ANR (French funding agency for research).

Patents

  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, WO2001014958A2, 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, with 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, with D. Bolignano, R. Marlet, Trusted Logic, WO2005073859, EP1702268, FR2864655.

Miscellaneous


Home page: http://gallium.inria.fr/~xleroy/