2024

Conference papers

ref_biblio

Xavier Leroy. Well-founded recursion done right. CoqPL 2024: The Tenth International Workshop on Coq for Programming Languages, ACM, Jan 2024, London, United Kingdom. ⟨hal-04356563v2⟩

Accès au texte intégral et bibtex

2023

Journal articles

ref_biblio

Xavier Leroy. Sciences du logiciel. L'Annuaire du Collège de France. Résumés des cours et travaux, 2023, 120, pp.13-22. ⟨10.4000/annuaire-cdf.18052⟩. ⟨hal-04245933⟩

Accès au bibtex

ref_biblio

Andrew W Appel, Xavier Leroy. Efficient Extensional Binary Tries. Journal of Automated Reasoning, 2023, 67, pp.Article number 8. ⟨10.1007/s10817-022-09655-x⟩. ⟨hal-03372247v4⟩

Accès au texte intégral et bibtex

Proceedings

ref_biblio

Dominique Charpin, Xavier Leroy. Déchiffrement(s) : des hiéroglyphes à l’ADN. Odile Jacob, pp.272, 2023, Colloque annuel du Collège de France, 978-2-415-00687-7. ⟨hal-04210865⟩

Accès au bibtex

Reports

ref_biblio

Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, et al.. The OCaml system release 5.1: Documentation and user's manual. [Intern report] Inria. 2023. ⟨hal-00930213v10⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. The CompCert C verified compiler: Documentation and user’s manual. [Intern report] Inria. 2023, pp.1-79. ⟨hal-01091802v11⟩

Accès au texte intégral et bibtex

2022

Journal articles

ref_biblio

Xavier Leroy. Sciences du logiciel. L'Annuaire du Collège de France. Résumés des cours et travaux, 2022, 119, pp.21-33. ⟨10.4000/annuaire-cdf.16737⟩. ⟨hal-04265123⟩

Accès au texte intégral et bibtex

2021

Journal articles

ref_biblio

Nathanaël Courant, Xavier Leroy. Verified Code Generation for the Polyhedral Model. Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.40:1-40:24. ⟨10.1145/3434321⟩. ⟨hal-03000244⟩

Accès au texte intégral et bibtex

2020

Books

ref_biblio

Xavier Leroy. Software, between mind and matter. Collège de France, 2020, Inaugural lecture at Collège de France. ⟨hal-02392159v2⟩

Accès au texte intégral et bibtex

2019

Conference papers

ref_biblio

Xavier Leroy. In Search of Software Perfection: An introduction to deductive software verification. BOB Summer 2019 Konferenz, Aug 2019, Berlin, Germany. ⟨hal-02392114⟩

Accès au bibtex

Books

ref_biblio

Xavier Leroy. Le logiciel, entre l’esprit et la matière : Leçon inaugurale prononcée au Collège de France le jeudi 15 novembre 2018. OpenEdition Books, 2019, 9782722605299. ⟨hal-02405754⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Le logiciel, entre l'esprit et la matière. Fayard, 284, 2019, Leçons inaugurales du Collège de France, 978-2-213-71241-3. ⟨hal-02370113⟩

Accès au bibtex

2018

Scientific blog post

ref_biblio

Xavier Leroy. À la recherche du logiciel parfait. 2018. ⟨hal-01966252⟩

Accès au bibtex

Conference papers

ref_biblio

Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, et al.. Embedded Program Annotations for WCET Analysis. WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, Jul 2018, Barcelona, Spain. ⟨10.4230/OASIcs.WCET.2018.8⟩. ⟨hal-01848686⟩

Accès au texte intégral et bibtex

ref_biblio

Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, et al.. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9. ⟨hal-01643290⟩

Accès au texte intégral et bibtex

2017

Scientific blog post

ref_biblio

Xavier Leroy. How I found a crash bug with hyperthreading in Intel's Skylake processors. 2017. ⟨hal-01620870⟩

Accès au bibtex

Conference papers

ref_biblio

Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, et al.. A Formally Verified Compiler for Lustre. PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2017, Barcelone, Spain. ⟨hal-01512286⟩

Accès au texte intégral et bibtex

ref_biblio

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. pp.163-180. ⟨hal-01399482⟩

Accès au texte intégral et bibtex

2016

Conference papers

ref_biblio

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, SEE, Jan 2016, Toulouse, France. ⟨hal-01238879⟩

Accès au texte intégral et bibtex

2015

Journal articles

ref_biblio

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩. ⟨hal-00862689v3⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. A formally-verified C static analyzer. POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩. ⟨hal-01078386⟩

Accès au texte intégral et bibtex

Proceedings

ref_biblio

Xavier Leroy, Alwen Tiu. CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs. Conference on Certified Programs and Proofs, Jan 2015, Mumbai, India. ACM, pp.184, 2015, 978-1-4503-3296-5. ⟨hal-01101937⟩

Accès au bibtex

2014

Conference papers

ref_biblio

Xavier Leroy. Compiler verification for fun and profit. FMCAD 2014 - Formal Methods in Computer-Aided Design, Oct 2014, Lausanne, Switzerland. pp.9. ⟨hal-01076547⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Formal proofs of code generation and verification tools. SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. pp.1-4, ⟨10.1007/978-3-319-10431-7_1⟩. ⟨hal-01059423⟩

Accès au texte intégral et bibtex

ref_biblio

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. pp.543-548, ⟨10.1007/978-3-319-08970-6_36⟩. ⟨hal-00981212⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Formal verification of a static analyzer: abstract interpretation in type theory. Types - The 2014 Types Meeting, May 2014, Paris, France. ⟨hal-00983847⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Proof assistants in computer science research. IHP thematic trimester on Semantics of proofs and certified mathematics, Institut Henri Poincaré, Apr 2014, Paris, France. ⟨hal-00983850⟩

Accès au bibtex

Book sections

ref_biblio

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⟩

Accès au bibtex

2013

Conference papers

ref_biblio

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115. ⟨hal-00743090v2⟩

Accès au texte intégral et bibtex

2012

Journal articles

ref_biblio

Andrew W. Appel, Robert Dockins, Xavier Leroy. A list-machine benchmark for mechanized metatheory. Journal of Automated Reasoning, 2012, 49 (3), pp.453--491. ⟨10.1007/s10817-011-9226-1⟩. ⟨hal-00674176⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Valentin Robert, Xavier Leroy. A formally-verified alias analysis. CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. pp.11-26, ⟨10.1007/978-3-642-35308-6_5⟩. ⟨hal-00773109⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Mechanized Semantics for Compiler Verification. APLAS 2012 - 10th Asian Symposium on Programming Languages and Systems, Dec 2012, Kyoto, Japan. pp.386-388, ⟨10.1007/978-3-642-35182-2_27⟩. ⟨hal-01079337⟩

Accès au texte intégral et bibtex

ref_biblio

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. pp.397-416, ⟨10.1007/978-3-642-28869-2_20⟩. ⟨hal-01077321⟩

Accès au texte intégral et bibtex

ref_biblio

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, AAAF, SEE, Feb 2012, Toulouse, France. ⟨hal-00653367⟩

Accès au texte intégral et bibtex

ref_biblio

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, ACM, Jan 2012, Philadelphia, PA, United States. pp.521-532, ⟨10.1145/2103656.2103718⟩. ⟨hal-00674663⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart. The CompCert Memory Model, Version 2. [Research Report] RR-7987, INRIA. 2012, pp.26. ⟨hal-00703441⟩

Accès au texte intégral et bibtex

2011

Journal articles

ref_biblio

Xavier Leroy. Safety First! (technical perspective). Communications of the ACM, 2011, 54 (12), pp.122. ⟨10.1145/2043174.2043196⟩. ⟨hal-01091803⟩

Accès au bibtex

Conference papers

ref_biblio

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. ⟨10.1109/CGO.2011.5764668⟩. ⟨hal-01091800⟩

Accès au texte intégral et bibtex

ref_biblio

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. pp.59-68, ⟨10.4230/OASIcs.PPES.2011.59⟩. ⟨inria-00551370⟩

Accès au texte intégral et bibtex

ref_biblio

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, ACM, Jan 2011, Austin, TX, United States. pp.67-79, ⟨10.1145/1926385.1926395⟩. ⟨hal-00674174⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Verified squared: does critical software deserve verified tools?. POPL 2011 - 38th symposium Principles of Programming Languages, Jan 2011, Austin, United States. pp.1-2, ⟨10.1145/1926385.1926387⟩. ⟨hal-01076682⟩

Accès au texte intégral et bibtex

2010

Journal articles

ref_biblio

Xavier Leroy. Comment faire confiance à un compilateur ?. Interstices, 2010. ⟨hal-01350287⟩

Accès au bibtex

ref_biblio

Xavier Leroy. Comment faire confiance à un compilateur ?. Les Cahiers de l'INRIA - La Recherche, 2010, Cancer la révolution, 440 avril 2010. ⟨inria-00511377⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Silvain Rideau, Xavier Leroy. Validating register allocation and spilling. Compiler Construction 2010, Mar 2010, Paphos, Cyprus. pp.224-243, ⟨10.1007/978-3-642-11970-5_13⟩. ⟨inria-00529841⟩

Accès au texte intégral et bibtex

ref_biblio

Jean-Baptiste Tristan, Xavier Leroy. A simple, verified validator for software pipelining. 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. ⟨10.1145/1706299.1706311⟩. ⟨inria-00529836⟩

Accès au texte intégral et bibtex

Book sections

ref_biblio

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⟩

Accès au texte intégral et bibtex

2009

Journal articles

ref_biblio

Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩. ⟨inria-00360768v3⟩

Accès au texte intégral et bibtex

ref_biblio

Zaynah Dargaye, Xavier Leroy. A verified framework for higher-order uncurrying optimizations. Higher-Order and Symbolic Computation, 2009, 22 (3), ⟨10.1007/s10990-010-9050-z⟩. ⟨hal-01499915⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52 (7), pp.107-115. ⟨10.1145/1538788.1538814⟩. ⟨inria-00415861⟩

Accès au texte intégral et bibtex

ref_biblio

Tom Hirschowitz, Xavier Leroy, J. B. Wells. Compilation of extended recursion in call-by-value functional languages. Higher-Order and Symbolic Computation, 2009, 22 (1), pp.3-66. ⟨10.1007/s10990-009-9042-z⟩. ⟨hal-00359213⟩

Accès au texte intégral et bibtex

ref_biblio

Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩. ⟨inria-00352524⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy, Hervé Grall. Coinductive big-step operational semantics. Information and Computation, 2009, 207 (2), pp.284-304. ⟨10.1016/j.ic.2007.12.004⟩. ⟨inria-00309010⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

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. pp.316-326, ⟨10.1145/1542476.1542512⟩. ⟨inria-00415865⟩

Accès au texte intégral et bibtex

2008

Journal articles

ref_biblio

Laurence Rideau, Bernard P. Serpette, Xavier Leroy. Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩. ⟨inria-00289709⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy, Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩. ⟨inria-00289542⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

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), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩. ⟨inria-00289540⟩

Accès au texte intégral et bibtex

2007

Conference papers

ref_biblio

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. pp.211-225, ⟨10.1007/978-3-540-75560-9_17⟩. ⟨inria-00289541⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy. A locally nameless solution to the POPLmark challenge. [Research Report] RR-6098, INRIA. 2007, pp.54. ⟨inria-00123945v2⟩

Accès au texte intégral et bibtex

Preprints, Working Papers, ...

ref_biblio

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

Accès au texte intégral et bibtex

2006

Conference papers

ref_biblio

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. pp.199-208, ⟨10.1109/ASE.2006.49⟩. ⟨hal-00149566⟩

Accès au texte intégral et bibtex

ref_biblio

Sandrine Blazy, Zaynah Dargaye, Xavier Leroy. Formal Verification of a C Compiler Front-end. FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩. ⟨inria-00106401⟩

Accès au texte intégral et bibtex

ref_biblio

Andrew W. 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. pp.95-108, ⟨10.1016/j.entcs.2007.01.020⟩. ⟨inria-00289543⟩

Accès au texte intégral et bibtex

ref_biblio

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.. Apr 2006, Porto Alegre, Brazil. pp.199-207. ⟨hal-00154357⟩

Accès au bibtex

ref_biblio

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. pp.7-20. ⟨hal-00154188⟩

Accès au bibtex

ref_biblio

Xavier Leroy. Coinductive big-step operational semantics. European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. pp.42-54, ⟨10.1007/11693024_5⟩. ⟨inria-00289545⟩

Accès au texte intégral et bibtex

ref_biblio

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. pp.42--54, ⟨10.1145/1111037.1111042⟩. ⟨inria-00000963⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Andrew W. W. Appel, Xavier Leroy. A list-machine benchmark for mechanized metatheory. [Research Report] RR-5914, INRIA. 2006. ⟨inria-00077531⟩

Accès au texte intégral et bibtex

2005

Journal articles

ref_biblio

Tom Hirschowitz, Xavier Leroy. Mixin modules in a call-by-value setting. ACM Transactions on Programming Languages and Systems (TOPLAS), 2005, 27 (5), pp.857 - 881. ⟨10.1145/1086642.1086644⟩. ⟨hal-00310317⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Sandrine Blazy, Xavier Leroy. Formal verification of a memory model for C-like imperative languages. ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. pp.280-299, ⟨10.1007/11576280⟩. ⟨inria-00077921⟩

Accès au texte intégral et bibtex

ref_biblio

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. ⟨hal-00699644⟩

Accès au bibtex

2004

Conference papers

ref_biblio

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. pp.66-81, ⟨10.1007/11617990⟩. ⟨inria-00289549⟩

Accès au texte intégral et bibtex

ref_biblio

Tom Hirschowitz, Xavier Leroy, J. B. Wells. Call-by-value mixin modules: Reduction semantics, side effects, types. European Symposium on Programming, 2004, Barcelona, Spain. pp.64-78, ⟨10.1007/b96702⟩. ⟨hal-00310123⟩

Accès au texte intégral et bibtex

2003

Journal articles

ref_biblio

Xavier Leroy. Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning, 2003, 30 (3-4), pp.235--269. ⟨10.1023/A:1025055424017⟩. ⟨hal-01499939⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Xavier Leroy. Computer Security from a Programming Language and Static Analysis Perspective. ESOP 2003: Programming Languages and Systems, 12th European Symposium on Programming, Apr 2003, Warsaw, Poland. pp.1 - 9, ⟨10.1007/3-540-36575-3_1⟩. ⟨hal-01499938⟩

Accès au texte intégral et bibtex

ref_biblio

Tom Hirschowitz, Xavier Leroy, J. B. Wells. Compilation of extended recursion in call-by-value functional languages. PPDP '03, 2003, Uppsala, Sweden. pp.160--171, ⟨10.1145/888251.888267⟩. ⟨hal-00310121⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

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⟩

Accès au texte intégral et bibtex

2002

Journal articles

ref_biblio

Xavier Leroy. Bytecode verification on Java smart cards. Software: Practice and Experience, 2002, 32 (4), pp.319-340. ⟨10.1002/spe.438⟩. ⟨hal-01499944⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Benjamin Grégoire, Xavier Leroy. A Compiled Implementation of Strong Reduction. ICFP '02: seventh ACM SIGPLAN international conference on Functional programming , ACM, Oct 2002, Pittsburgh, United States. pp.235-246, ⟨10.1145/581478.581501⟩. ⟨hal-01499941⟩

Accès au texte intégral et bibtex

ref_biblio

Tom Hirschowitz, Xavier Leroy. Mixin modules in a call-by-value setting. European Symposium on Programming, 2002, Grenoble, France. pp.207-236, ⟨10.1007/3-540-45927-8⟩. ⟨hal-00310119⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Tom Hirschowitz, Xavier Leroy, Joe B. Wells. A reduction semantics for call-by-value mixin modules. [Research Report] RR-4682, INRIA. 2002. ⟨inria-00071903⟩

Accès au texte intégral et bibtex

2001

Conference papers

ref_biblio

Xavier Leroy. On-card Bytecode Verification for Java Card. Smart card programming and security, proceedings E-Smart 2001, Sep 2001, Cannes, France. pp.150-164, ⟨10.1007/3-540-45418-7_13⟩. ⟨hal-01499956⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Java bytecode verification: an overview. Computer Aided Verification, CAV 2001, Jul 2001, Paris, France. pp.265-285, ⟨10.1007/3-540-44585-4_26⟩. ⟨hal-01499955⟩

Accès au texte intégral et bibtex

Software

ref_biblio

Xavier Leroy, Damien Doligez, Jérôme Vouillon, Alain Deutsch, Bruno Blanchet. OCamlStack 1.05.1. 2001, ⟨swh:1:dir:53c27f53e2115f847f855b9a400169d218363185;origin=https://hal.archives-ouvertes.fr/hal-01867778;visit=swh:1:snp:66f78f3d525323f8a6a0b9b4c9162be9a06d6481;anchor=swh:1:rev:7eec094cb90a3972ac86bea5789f3441003a3f2c;path=/⟩. ⟨hal-01867778⟩

Accès au texte intégral et bibtex

2000

Journal articles

ref_biblio

Xavier Leroy, François Pessaux. Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems (TOPLAS), 2000, 22 (2), pp.340-377. ⟨10.1145/349214.349230⟩. ⟨hal-01499948⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. A modular module system. Journal of Functional Programming, 2000, 10 (3), pp.269-303. ⟨10.1017/S0956796800003683⟩. ⟨hal-01499946⟩

Accès au texte intégral et bibtex

1999

Conference papers

ref_biblio

François Pessaux, Xavier Leroy. Type-based analysis of uncaught exceptions. POPL 1999: 26th symposium Principles of Programming Languages, ACM, Jan 1999, San Antonio, United States. pp.276 - 290, ⟨10.1145/292540.292565⟩. ⟨hal-01499959⟩

Accès au texte intégral et bibtex

Book sections

ref_biblio

Xavier Leroy, François Rouaix. Security properties of typed applets. Jan Vitek; Christian D. Jensen Secure Internet Programming - Security issues for Mobile and Distributed Objects, 1603, Springer, pp.147-182, 1999, LNCS, 978-3-540-66130-6. ⟨10.1007/3-540-48749-2_7⟩. ⟨hal-01499957⟩

Accès au texte intégral et bibtex

1998

Conference papers

ref_biblio

Marco Danelutto, Roberto Di Cosmo, Xavier Leroy, Susanna Pelagatti. Parallel Functional Programming with Skeletons: the OCamlP3L experiment. ACM Workshop on ML and its applications, ACM, Sep 1998, Baltimore, United States. ⟨hal-01499962⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. An overview of Types in Compilation. TIC 1998: workshop Types in Compilation, Mar 1998, Kyoto, Japan. pp.1-8, ⟨10.1007/BFb0055509⟩. ⟨hal-01499960⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy, François Rouaix. Security properties of typed applets. POPL 1998: 25th symposium Principles of Programming Languages, Jan 1998, San Diego, United States. pp.391-403, ⟨10.1145/268946.268979⟩. ⟨hal-01499963⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy, François Pessaux. Type-Based Analysis of Uncaught Exceptions. [Research Report] RR-3541, INRIA. 1998. ⟨inria-00073144⟩

Accès au texte intégral et bibtex

Software

ref_biblio

Bruno Blanchet, Xavier Leroy, Damien Doligez, François Rouaix, Jérôme Vouillon, et al.. CamlDim. 1998, ⟨swh:1:dir:f82b87d50c6b60741d85de0a83ec0982112bdee0;origin=https://hal.archives-ouvertes.fr/hal-01863457;visit=swh:1:snp:4d172a103aed92c68e0fd3b3be8c4a6e058d670d;anchor=swh:1:rev:c812045b6b43f7bfeca7954a47baf2dcbb8c6d8d;path=/⟩. ⟨hal-01863457⟩

Accès au texte intégral et bibtex

1997

Conference papers

ref_biblio

Xavier Leroy. The effectiveness of type-based unboxing. TIC 1997: Workshop Types in Compilation, Jun 1997, Amsterdam, Netherlands. ⟨hal-01499964⟩

Accès au texte intégral et bibtex

1996

Journal articles

ref_biblio

Xavier Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 1996, 6 (5), pp.667 - 698. ⟨10.1017/S0956796800001933⟩. ⟨hal-01499965⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy. A Modular Module System. [Research Report] RR-2866, INRIA. 1996. ⟨inria-00073825⟩

Accès au texte intégral et bibtex

1995

Conference papers

ref_biblio

Xavier Leroy. Applicative functors and fully transparent higher-order modules. POPL 1995: 22nd symposium Principles of Programming Languages, ACM, Jan 1995, San Francisco, United States. pp.142 - 153, ⟨10.1145/199448.199476⟩. ⟨hal-01499966⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy. A syntactic theory of type generativity and sharing. [Research Report] RR-2545, INRIA. 1995. ⟨inria-00074133⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Le système Caml Special Light: modules et compilation efficace en Caml. [Rapport de recherche] RR-2721, INRIA. 1995. ⟨inria-00073972⟩

Accès au texte intégral et bibtex

1994

Conference papers

ref_biblio

Maria-Virginia Aponte, Xavier Leroy. Llamado de procedimientos a distancia y abstracción de tipos. 20th CLEI PANEL latino-american computer science conference, Aug 1994, Mexico, México. pp.1281-1292. ⟨hal-01499967⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Manifest types, modules, and separate compilation. POPL 1994: 21st symposium Principles of Programming Languages, ACM, Jan 1994, Portland, United States. pp.109-122, ⟨10.1145/174675.176926⟩. ⟨hal-01499976⟩

Accès au texte intégral et bibtex

1993

Journal articles

ref_biblio

Xavier Leroy, Michel Mauny. Dynamics in ML. Journal of Functional Programming, 1993, 3 (4), pp.431-463. ⟨10.1017/S0956796800000848⟩. ⟨hal-01499972⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Xavier Leroy. Polymorphism by name for references and continuations. POPL 1993: 20th symposium Principles of Programming Languages, Jan 1993, Charleston, United States. pp.220-231, ⟨10.1145/158511.158632⟩. ⟨hal-01499970⟩

Accès au texte intégral et bibtex

ref_biblio

Damien Doligez, Xavier Leroy. A concurrent, generational garbage collector for a multithreaded implementation of ML. POPL 1993: 20th symposium Principles of Programming Languages, Jan 1993, Charleston, United States. pp.113-123, ⟨10.1145/158511.158611⟩. ⟨hal-01499969⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy. Programmation du systeme Unix en Caml Light. RT-0147, INRIA. 1993, pp.91. ⟨inria-00070021⟩

Accès au texte intégral et bibtex

1992

Conference papers

ref_biblio

Xavier Leroy. Unboxed objects and polymorphic typing. POPL 1992: 19th symposium Principles of Programming Languages, Jan 1992, Albuquerque, United States. pp.177-188, ⟨10.1145/143165.143205⟩. ⟨hal-01499973⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy. Polymorphic typing of an algorithmic language. [Research Report] RR-1778, INRIA. 1992. ⟨inria-00077018⟩

Accès au texte intégral et bibtex

Theses

ref_biblio

Xavier Leroy. Typage polymorphe d'un langage algorithmique. Langage de programmation [cs.PL]. Université Paris 7, 1992. Français. ⟨NNT : ⟩. ⟨tel-01499951⟩

Accès au texte intégral et bibtex

1991

Conference papers

ref_biblio

Xavier Leroy, Michel Mauny. Dynamics in ML. FPCA 1991: Functional Programming Languages and Computer Architecture, Aug 1991, Boston, United States. pp.406-426. ⟨hal-01499984⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy, Pierre Weis. Polymorphic type inference and assignment. POPL 1991: 18th symposium Principles of Programming Languages, ACM, Jan 1991, Orlando, United States. pp.291-302, ⟨10.1145/99583.99622⟩. ⟨hal-01499974⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy, Michel Mauny. Dynamics in ML. [Research Report] RR-1491, INRIA. 1991. ⟨inria-00075071⟩

Accès au texte intégral et bibtex

1990

Conference papers

ref_biblio

Xavier Leroy. Efficient data representation in polymorphic languages. PLILP 1990: Programming Language Implementation and Logic Programming, Aug 1990, Linköping, Sweden. ⟨10.1007/BFb0024189⟩. ⟨hal-01499983⟩

Accès au texte intégral et bibtex

ref_biblio

Luca Cardelli, Xavier Leroy. Abstract types and the dot notation. IFIP TC2 working conference on programming concepts and methods, IFIP, Apr 1990, Tiberias, Israel. pp.479-504. ⟨hal-01499980⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Xavier Leroy, Pierre Weis. Polymorphic type inference and assignment. RR-1327, INRIA. 1990. ⟨inria-00075233⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. Efficient data representation in polymorphic languages. RR-1264, INRIA. 1990. ⟨inria-00075295⟩

Accès au texte intégral et bibtex

ref_biblio

Xavier Leroy. The ZINC experiment : an economical implementation of the ML language. RT-0117, INRIA. 1990, pp.100. ⟨inria-00070049⟩

Accès au texte intégral et bibtex