Publications HAL

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
BibTex

Books

ref_biblio
Xavier Leroy. Software, between mind and matter. 2019, Inaugural lecture at Collège de France. ⟨hal-02392159⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02392159/file/plain.pdf 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
BibTex

Reports

ref_biblio
Xavier Leroy. The CompCert C verified compiler: Documentation and user’s manual: Version 3.6. [Intern report] Inria. 2019, pp.1-78. ⟨hal-01091802v7⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091802/file/manual.pdf BibTex
ref_biblio
Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, et al.. The OCaml system release 4.09: Documentation and user's manual. [Intern report] Inria. 2019, pp.1-789. ⟨hal-00930213v6⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00930213/file/ocaml-4.09-refman.pdf BibTex

2018

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
https://hal.inria.fr/hal-01848686/file/wcet2018_embedded_program_annotations.pdf 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
https://hal.inria.fr/hal-01643290/file/ERTS_2018_paper_59.pdf BibTex

Other publications

ref_biblio
Xavier Leroy. À la recherche du logiciel parfait. 2018. ⟨hal-01966252⟩
Accès au bibtex
BibTex

2017

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
https://hal.inria.fr/hal-01512286/file/velus-pldi17.pdf 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
https://hal.inria.fr/hal-01399482/file/SSS2017_kaestner_et_al.pdf BibTex

Other publications

ref_biblio
Xavier Leroy. How I found a crash bug with hyperthreading in Intel's Skylake processors. 2017. ⟨hal-01620870⟩
Accès au bibtex
BibTex

2016

Journal articles

ref_biblio
Anaïs Fradet, Mathilde Bouchet, Carine Delliaux, Manon Gervais, Casina Kan, et al.. Estrogen related receptor alpha in castration-resistant prostate cancer cells promotes tumor progression in bone. Oncotarget, Impact journals, 2016, 7 (47), pp.77071-77086. ⟨10.18632/oncotarget.12787⟩. ⟨hal-02353264⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02353264/file/oncotarget-07-77071.pdf BibTex

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
https://hal.inria.fr/hal-01238879/file/erts2016_compcert.pdf 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, Springer Verlag, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩. ⟨hal-00862689v3⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00862689/file/floating-point-compcert.pdf 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
https://hal.inria.fr/hal-01078386/file/verasco-popl2015.pdf BibTex

Directions of work or 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
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
https://hal.inria.fr/hal-01076547/file/FMCAD14-Leroy.pdf 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
https://hal.inria.fr/hal-01059423/file/abstract.pdf 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
https://hal.inria.fr/hal-00981212/file/Formal-C-CompCert.pdf 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
https://hal.inria.fr/hal-00983847/file/invited-2.pdf 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
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
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
https://hal.inria.fr/hal-00743090/file/article.pdf BibTex

2012

Journal articles

ref_biblio
Andrew Appel, Robert Dockins, Xavier Leroy. A list-machine benchmark for mechanized metatheory. Journal of Automated Reasoning, Springer Verlag, 2012, 49 (3), pp.453--491. ⟨10.1007/s10817-011-9226-1⟩. ⟨hal-00674176⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00674176/file/listmachine-journal.pdf 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
https://hal.inria.fr/hal-00773109/file/alias-analysis.pdf 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
https://hal.inria.fr/hal-01079337/file/mechanized-semantics-aplas-cpp-2012.pdf 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
https://hal.inria.fr/hal-01077321/file/validated-parser.pdf 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
https://hal.inria.fr/hal-00653367/file/erts2012.pdf 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
https://hal.inria.fr/hal-00674663/file/cpp-construction.pdf BibTex

Reports

ref_biblio
Xavier Leroy, Andrew 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
https://hal.inria.fr/hal-00703441/file/RR-7987.pdf BibTex

2011

Journal articles

ref_biblio
Xavier Leroy. Safety First! (technical perspective). Communications of the ACM, ACM, 2011, 54 (12), pp.122. ⟨10.1145/2043174.2043196⟩. ⟨hal-01091803⟩
Accès au bibtex
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
https://hal.inria.fr/hal-01091800/file/abstract.pdf 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
https://hal.inria.fr/inria-00551370/file/pppes2011_2112.pdf 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
https://hal.inria.fr/hal-01076682/file/popl11-invited-talk.pdf 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
https://hal.inria.fr/hal-00674174/file/cpp-object-layout.pdf BibTex

2010

Journal articles

ref_biblio
Xavier Leroy. Comment faire confiance à un compilateur ?. Interstices, INRIA, 2010. ⟨hal-01350287⟩
Accès au bibtex
BibTex
ref_biblio
Xavier Leroy. Comment faire confiance à un compilateur ?. Les Cahiers de l'INRIA - La Recherche, INRIA, 2010, Cancer la révolution. ⟨inria-00511377⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00511377/file/inria-n440-avril10.pdf 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
https://hal.inria.fr/inria-00529841/file/validation-regalloc.pdf 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
https://hal.inria.fr/inria-00529836/file/validation-softpipe.pdf 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
https://hal.inria.fr/inria-00529848/file/notes.pdf BibTex

2009

Journal articles

ref_biblio
Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩. ⟨inria-00360768v3⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00360768/file/paper2.pdf BibTex
ref_biblio
Zaynah Dargaye, Xavier Leroy. A verified framework for higher-order uncurrying optimizations. Higher-Order and Symbolic Computation, Springer Verlag, 2009, 22 (3), ⟨10.1007/s10990-010-9050-z⟩. ⟨hal-01499915⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499915/file/higher-order-uncurrying.pdf BibTex
ref_biblio
Xavier Leroy. Formal verification of a realistic compiler. Communications- ACM, Association for Computing Machinery, 2009, 52 (7), pp.107-115. ⟨10.1145/1538788.1538814⟩. ⟨inria-00415861⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00415861/file/compcert-CACM.pdf BibTex
ref_biblio
Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, Springer Verlag, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩. ⟨inria-00352524⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00352524/file/paper.pdf BibTex
ref_biblio
Xavier Leroy, Hervé Grall. Coinductive big-step operational semantics. Information and Computation, Elsevier, 2009, 207 (2), pp.284-304. ⟨10.1016/j.ic.2007.12.004⟩. ⟨inria-00309010⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00309010/file/leroy-grall.pdf 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, Springer Verlag, 2009, 22 (1), pp.3-66. ⟨10.1007/s10990-009-9042-z⟩. ⟨hal-00359213⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00359213/file/letrec.pdf 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
https://hal.inria.fr/inria-00415865/file/validation-LCM.pdf BibTex

2008

Journal articles

ref_biblio
Laurence Rideau, Bernard Serpette, Xavier Leroy. Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩. ⟨inria-00289709⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289709/file/parallel-move.pdf 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, Springer Verlag, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩. ⟨inria-00289542⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289542/file/memory-model-journal.pdf 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
https://hal.inria.fr/inria-00289540/file/validation-scheduling.pdf 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
https://hal.inria.fr/inria-00289541/file/cps-dargaye-leroy.pdf 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
https://hal.inria.fr/inria-00123945/file/RR-6098.pdf BibTex

Preprints, Working Papers, ...

ref_biblio
Laurence Rideau, Bernard 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
https://hal.inria.fr/inria-00176007/file/pmov.pdf 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
https://hal.archives-ouvertes.fr/hal-00149566/file/ase.pdf 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
https://hal.inria.fr/inria-00106401/file/fm06Blazy.pdf BibTex
ref_biblio
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. pp.95-108, ⟨10.1016/j.entcs.2007.01.020⟩. ⟨inria-00289543⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289543/file/listmachine-lfmtp.pdf 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
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
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
https://hal.inria.fr/inria-00289545/file/coindsem.pdf 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
https://hal.inria.fr/inria-00000963/file/compiler-certif.pdf BibTex

Reports

ref_biblio
Andrew 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
https://hal.inria.fr/inria-00077531/file/RR-5914.pdf 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), ACM, 2005, 27 (5), pp.857 - 881. ⟨10.1145/1086642.1086644⟩. ⟨hal-00310317⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00310317/file/cmsv-long.pdf 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
https://hal.inria.fr/inria-00077921/file/icfem05Blazy.pdf 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
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
https://hal.inria.fr/inria-00289549/file/proofs_dataflow_optimizations.pdf 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
https://hal.archives-ouvertes.fr/hal-00310123/file/cbv-mixins.pdf BibTex

2003

Journal articles

ref_biblio
Xavier Leroy. Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning, Springer Verlag, 2003, 30 (3-4), pp.235--269. ⟨10.1023/A:1025055424017⟩. ⟨hal-01499939⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499939/file/bytecode-verification-JAR.pdf 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
https://hal.inria.fr/hal-01499938/file/language-security-etaps03.pdf 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
https://hal.archives-ouvertes.fr/hal-00310121/file/compil-recursion.pdf 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
https://hal.inria.fr/inria-00071858/file/RR-4728.pdf BibTex

2002

Journal articles

ref_biblio
Xavier Leroy. Bytecode verification on Java smart cards. Software: Practice and Experience, Wiley, 2002, 32 (4), pp.319-340. ⟨10.1002/spe.438⟩. ⟨hal-01499944⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499944/file/oncard-verifier-spe.pdf 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
https://hal.inria.fr/hal-01499941/file/strong-reduction.pdf 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
https://hal.archives-ouvertes.fr/hal-00310119/file/mixins-cbv-esop2002.pdf 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
https://hal.inria.fr/inria-00071903/file/RR-4682.pdf 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
https://hal.inria.fr/hal-01499956/file/oncard-verifier-esmart.pdf 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
https://hal.inria.fr/hal-01499955/file/survey-bytecode-verification.pdf 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⟩. ⟨hal-01867778⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01867778/file/ocamlstack1.05.1.zip BibTex

2000

Journal articles

ref_biblio
Xavier Leroy. A modular module system. Journal of Functional Programming, Cambridge University Press (CUP), 2000, 10 (3), pp.269-303. ⟨10.1017/S0956796800003683⟩. ⟨hal-01499946⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499946/file/modular-modules-jfp.pdf BibTex
ref_biblio
Xavier Leroy, François Pessaux. Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2000, 22 (2), pp.340-377. ⟨10.1145/349214.349230⟩. ⟨hal-01499948⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499948/file/exceptions-toplas.pdf 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
https://hal.inria.fr/hal-01499959/file/exceptions-popl.pdf 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
https://hal.inria.fr/hal-01499957/file/sip-typed-applets.pdf 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
https://hal.inria.fr/hal-01499962/file/ocamlp3l-mlws.pdf 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
https://hal.inria.fr/hal-01499960/file/intro-tic98.pdf 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
https://hal.inria.fr/hal-01499963/file/typed-applets.pdf 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
https://hal.inria.fr/inria-00073144/file/RR-3541.pdf 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⟩. ⟨hal-01863457⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01863457/file/camldim74.zip 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
https://hal.inria.fr/hal-01499964/file/unboxing-tic97.pdf BibTex

1996

Journal articles

ref_biblio
Xavier Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, Cambridge University Press (CUP), 1996, 6 (5), pp.667 - 698. ⟨10.1017/S0956796800001933⟩. ⟨hal-01499965⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499965/file/syntactic-generativity.pdf 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
https://hal.inria.fr/inria-00073825/file/RR-2866.pdf 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
https://hal.inria.fr/hal-01499966/file/applicative-functors.pdf 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
https://hal.inria.fr/inria-00074133/file/RR-2545.pdf 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
https://hal.inria.fr/inria-00073972/file/RR-2721.pdf BibTex

1994

Conference papers

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
https://hal.inria.fr/hal-01499976/file/manifest-types-popl.pdf BibTex

1993

Journal articles

ref_biblio
Xavier Leroy, Michel Mauny. Dynamics in ML. Journal of Functional Programming, Cambridge University Press (CUP), 1993, 3 (4), pp.431-463. ⟨10.1017/S0956796800000848⟩. ⟨hal-01499972⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499972/file/dynamics-in-ML.pdf 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
https://hal.inria.fr/hal-01499970/file/polymorphism-by-name.pdf 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
https://hal.inria.fr/hal-01499969/file/concurrent-gc.pdf 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
https://hal.inria.fr/inria-00070021/file/RT-0147.pdf 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
https://hal.inria.fr/hal-01499973/file/unboxed-polymorphism.pdf 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
https://hal.inria.fr/inria-00077018/file/RR-1778.pdf BibTex

Theses

ref_biblio
Xavier Leroy. Typage polymorphe d'un langage algorithmique. Langage de programmation [cs.PL]. Université Paris 7, 1992. Français. ⟨tel-01499951⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01499951/file/these-doctorat.pdf 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
https://hal.inria.fr/hal-01499984/file/dynamics-in-ML-fpca.pdf 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
https://hal.inria.fr/hal-01499974/file/polymorphic-assignment.pdf 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
https://hal.inria.fr/inria-00075071/file/RR-1491.pdf 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
https://hal.inria.fr/hal-01499983/file/data-representation-plilp.pdf 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
https://hal.inria.fr/hal-01499980/file/abstract-types-dot-notation.pdf 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
https://hal.inria.fr/inria-00075233/file/RR-1327.pdf 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
https://hal.inria.fr/inria-00075295/file/RR-1264.pdf 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
https://hal.inria.fr/inria-00070049/file/RT-0117.pdf BibTex