Nombre de documents

67

CV de Xavier Leroy


Communication dans un congrès32 documents

  • Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, et al.. Closing the Gap – The Formally Verified Optimizing Compiler CompCert. SSS'17: Safety-critical Systems Symposium 2017, Feb 2017, Bristol, United Kingdom. CreateSpace, pp.163-180, 2017, Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium. <hal-01399482>
  • Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, et al.. CompCert - A Formally Verified Optimizing Compiler. ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse, France. <http://www.erts2016.org/>. <hal-01238879>
  • Xavier Leroy. Formal proofs of code generation and verification tools. Dimitra Giannakopoulou and Gwen Salaün. SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. Springer, 8702, pp.1-4, 2014, Lecture Notes in Computer Science. <10.1007/978-3-319-10431-7_1>. <hal-01059423>
  • Robbert Krebbers, Xavier Leroy, Freek Wiedijk. Formal C semantics: CompCert and the C standard. ITP 2014: Fifth conference on Interactive Theorem Proving, Jul 2014, Vienna, Austria. Springer, 8558, pp.543-548, 2014, Lecture Notes in Computer Science. <10.1007/978-3-319-08970-6_36>. <hal-00981212>
  • Xavier Leroy. Proof assistants in computer science research. IHP thematic trimester on Semantics of proofs and certified mathematics, Apr 2014, Paris, France. 2014. <hal-00983850>
  • Xavier Leroy. Formal verification of a static analyzer: abstract interpretation in type theory. Types - The 2014 Types Meeting, May 2014, Paris, France. 2014. <hal-00983847>
  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. IEEE, pp.107-115, 2013. <hal-00743090v2>
  • Valentin Robert, Xavier Leroy. A formally-verified alias analysis. Hawblitzel, Chris and Miller, Dale. CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. Springer, 7679, pp.11-26, 2012, Lecture Notes in Computer Science; Certified Programs and Proofs. <10.1007/978-3-642-35308-6_5>. <hal-00773109>
  • Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, et al.. Formally verified optimizing compilation in ACG-based flight control software. ERTS2 2012: Embedded Real Time Software and Systems, Feb 2012, Toulouse, France. 2012. <hal-00653367>
  • Jacques-Henri Jourdan, François Pottier, Xavier Leroy. Validating LR(1) Parsers. ESOP 2012 - Programming Languages and Systems - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. Springer, 7211, pp.397-416, Lecture Notes in Computer Science. <10.1007/978-3-642-28869-2_20>. <hal-01077321>
  • Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy. A mechanized semantics for C++ object construction and destruction, with applications to resource management. POPL '12 - 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2012, Philadelphia, PA, United States. pp.521-532, 2012, <10.1145/2103656.2103718>. <hal-00674663>
  • Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris. Towards Formally Verified Optimizing Compilation in Flight Control Software. PPES 2011: Predictability and Performance in Embedded Systems, Mar 2011, Grenoble, France. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, 18, pp.59-68, 2011, OpenAccess Series in Informatics. <10.4230/OASIcs.PPES.2011.59>. <inria-00551370>
  • Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy. Formal verification of object layout for C++ multiple inheritance. POPL'11 - 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2011, Austin, TX, United States. ACM Press, pp.67-79, 2011, <10.1145/1926385.1926395>. <hal-00674174>
  • Xavier Leroy. Formally verifying a compiler: Why? How? How far?. CGO 2011 - 9th Annual IEEE/ACM International Symposium on Code Generation and Optimization, Apr 2011, Chamonix, France. IEEE, <10.1109/CGO.2011.5764668>. <hal-01091800>
  • Jean-Baptiste Tristan, Xavier Leroy. A simple, verified validator for software pipelining. ACM. 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. 2010, <10.1145/1706299.1706311>. <inria-00529836>
  • Silvain Rideau, Xavier Leroy. Validating register allocation and spilling. Compiler Construction 2010, Mar 2010, Paphos, Cyprus. Springer, 6011, pp.224-243, 2010, Lecture Notes in Computer Science; Compiler Construction 19th International Conference, CC 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. <10.1007/978-3-642-11970-5_13>. <inria-00529841>
  • Jean-Baptiste Tristan, Xavier Leroy. Verified Validation of Lazy Code Motion. ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), Jun 2009, Dublin, Ireland. ACM, pp.316-326, 2009, <10.1145/1542476.1542512>. <inria-00415865>
  • Jean-Baptiste Tristan, Xavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. 35th ACM Symposium on Principles of Programming Languages (POPL 2008), Jan 2008, San Francisco, United States. ACM Press, pp.17-27, 2008, <10.1145/1328438.1328444>. <inria-00289540>
  • Zaynah Dargaye, Xavier Leroy. Mechanized verification of CPS transformations. Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, Oct 2007, Erevan, Armenia. Springer, 4790, pp.211-225, 2007, Lecture Notes in Artificial Intelligence; Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007. <10.1007/978-3-540-75560-9_17>. <inria-00289541>
  • Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, Jérôme Vouillon. Maintaining large software distributions: new challenges from the FOSS era.. Apr 2006, Vienna, Austria. EASST, pp.7-20, 2006, EASST Newsletter, volume 12. <hal-00154188>
  • Roberto Di Cosmo, Jaap Boender, Berke Durak, Xavier Leroy, Fabio Mancinelli, et al.. News from the EDOS project: improving the maintenance of free software distributions.. Olivier Berger. Apr 2006, Porto Alegre, Brazil. Brazilian Computer Society, pp.199-207, 2006. <hal-00154357>
  • Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. 33rd Symposium Principles of Programming Languages (POPL 2006), Jan 2006, Charleston, SC, United States. ACM Press, pp.42--54, 2006, <10.1145/1111037.1111042>. <inria-00000963>
  • Fabio Mancinelli, Jaap Boender, Roberto Di Cosmo, Jérôme Vouillon, Berke Durak, et al.. Managing the Complexity of Large Free and Open Source Package-Based Software Distributions. 21st IEEE/ACM International Conference on Automated Software Engineering, Sep 2006, Tokyo, Japan. ACM, pp.199-208, 2006, <10.1109/ASE.2006.49>. <hal-00149566>
  • Xavier Leroy. Coinductive big-step operational semantics. Peter Sestoft. European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. Springer, 3924, pp.42-54, 2006, Lecture Notes in Computer Science; Programming Languages and Systems. 15th European Symposium on Programming, ESOP 2006. <10.1007/11693024_5>. <inria-00289545>
  • Andrew W. Appel, Xavier Leroy. A list-machine benchmark for mechanized metatheory (extended abstract). Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. Elsevier, 174/5, pp.95-108, 2006, Electronic Notes in Theoretical Computer Science; Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006). <10.1016/j.entcs.2007.01.020>. <inria-00289543>
  • Sandrine Blazy, Zaynah Dargaye, Xavier Leroy. Formal Verification of a C Compiler Front-end. Jayadev Misra, Tobias Nipkow and Emil Sekerinski. FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. Springer-Verlag, 4085 (4085), pp.460-475, 2006, Lecture Notes in Computer Science; FM 2006: Formal Methods. <10.1007/11813040_31>. <inria-00106401>
  • Sandrine Blazy, Xavier Leroy. Formal verification of a memory model for C-like imperative languages. Kung-Kiu Lau, Richard Banach. ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. Springer, 3785 (3785), pp.280-299, 2005, Lecture Notes in Computer Science; Formal Methods and Software Engineering. <10.1007/11576280>. <inria-00077921>
  • Serge Abiteboul, Xavier Leroy, Boris Vrdoljak, Ciaran Bryce, Roberto Di Cosmo, et al.. EDOS: Environment for the Development and Distribution of Open Source Software. OSS 2005 - The First International Conference on Open Source Systems, Jul 2005, Genova, Italy. 2005. <hal-00699644>
  • Tom Hirschowitz, Xavier Leroy, J. B. Wells. Call-by-value mixin modules: Reduction semantics, side effects, types. European Symposium on Programming, 2004, Barcelona, Spain. Springer, 2986, pp.64-78, 2004, Lecture Notes in Computer Science. <10.1007/b96702>. <hal-00310123>
  • Yves Bertot, Benjamin Grégoire, Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. Springer, 3839, pp.66-81, 2006, Lecture Notes in Computer Science; Types for Proofs and Programs International Workshop, TYPES 2004, Revised Selected Papers. <10.1007/11617990>. <inria-00289549>
  • Tom Hirschowitz, Xavier Leroy, J. B. Wells. Compilation of extended recursion in call-by-value functional languages. PPDP '03, 2003, Uppsala, Sweden. ACM, pp.160--171, 2003, <10.1145/888251.888267>. <hal-00310121>
  • Tom Hirschowitz, Xavier Leroy. Mixin modules in a call-by-value setting. European Symposium on Programming, 2002, Grenoble, France. Springer, 2305, pp.207-236, 2002, Lecture Notes in Computer Science. <10.1007/3-540-45927-8>. <hal-00310119>

Rapport17 documents

  • Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, et al.. The OCaml system release 4.04: Documentation and user's manual. [Intern report] Inria. 2016. <hal-00930213v3>
  • Xavier Leroy. The CompCert C verified compiler: Documentation and user’s manual: Version 2.7. [Intern report] Inria. 2016. <hal-01091802v4>
  • Xavier Leroy, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert Memory Model, Version 2. [Research Report] RR-7987, INRIA. 2012, pp.26. <hal-00703441>
  • Xavier Leroy. A locally nameless solution to the POPLmark challenge. [Research Report] RR-6098, INRIA. 2007, pp.54. <inria-00123945v2>
  • Andrew W. Appel, Xavier Leroy. A list-machine benchmark for mechanized metatheory. [Research Report] RR-5914, INRIA. 2006. <inria-00077531>
  • Tom Hirschowitz, Xavier Leroy, J. B. Wells. On the implementation of recursion in call-by-value functional languages. [Research Report] RR-4728, INRIA. 2003. <inria-00071858>
  • Tom Hirschowitz, Xavier Leroy, Joe B. Wells. A reduction semantics for call-by-value mixin modules. [Research Report] RR-4682, INRIA. 2002. <inria-00071903>
  • Xavier Leroy, François Pessaux. Type-Based Analysis of Uncaught Exceptions. [Research Report] RR-3541, INRIA. 1998. <inria-00073144>
  • Xavier Leroy. A Modular Module System. [Research Report] RR-2866, INRIA. 1996. <inria-00073825>
  • Xavier Leroy. A syntactic theory of type generativity and sharing. [Research Report] RR-2545, INRIA. 1995. <inria-00074133>
  • Xavier Leroy. Le système Caml Special Light: modules et compilation efficace en Caml. [Rapport de recherche] RR-2721, INRIA. 1995. <inria-00073972>
  • Xavier Leroy. Programmation du systeme Unix en Caml Light. RT-0147, INRIA. 1993, pp.91. <inria-00070021>
  • Xavier Leroy. Polymorphic typing of an algorithmic language. [Research Report] RR-1778, INRIA. 1992. <inria-00077018>
  • Xavier Leroy, Michel Mauny. Dynamics in ML. [Research Report] RR-1491, INRIA. 1991. <inria-00075071>
  • Xavier Leroy. The ZINC experiment : an economical implementation of the ML language. RT-0117, INRIA. 1990, pp.100. <inria-00070049>
  • Xavier Leroy. Efficient data representation in polymorphic languages. RR-1264, INRIA. 1990. <inria-00075295>
  • Xavier Leroy, Pierre Weis. Polymorphic type inference and assignment. RR-1327, INRIA. 1990. <inria-00075233>

Direction d'ouvrage, Proceedings1 document

Article dans une revue14 documents

Chapitre d'ouvrage2 documents

  • Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart. The CompCert memory model. Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010. <hal-00905435>
  • Xavier Leroy. Mechanized semantics. J. Esparza and B. Spanfelner and O. Grumberg. Logics and languages for reliability and security, 25, IOS Press, pp.195-224, 2010, NATO Science for Peace and Security Series D: Information and Communication Security, <10.3233/978-1-60750-100-8-195>. <inria-00529848>

Pré-publication, Document de travail1 document

  • Laurence Rideau, Bernard Serpette, Xavier Leroy. Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves. 2007. <inria-00176007>