Publications HAL

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. Dagstuhl Publishing, OpenAccess Series in Informatics, 63, 〈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, Jan 2018, Toulouse, France. pp.1-9, 2018, 〈https://www.erts2018.org/〉. 〈hal-01643290〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01643290/file/ERTS_2018_paper_59.pdf BibTex

Reports

ref_biblio
Xavier Leroy. The CompCert C verified compiler: Documentation and user’s manual: Version 3.4. [Intern report] Inria. 2018, pp.1-77. 〈hal-01091802v6〉
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.07: Documentation and user's manual. [Intern report] Inria. 2018, pp.1-752. 〈hal-00930213v5〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00930213/file/ocaml-4.07-refman.pdf 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, Jun 2017, Barcelone, Spain. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, 〈http://pldi17.sigplan.og〉. 〈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. CreateSpace, pp.163-180, 2017, Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium. 〈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. News article at The Next Web (\url). 2017. 〈hal-01620870〉
Accès au bibtex
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, Jan 2016, Toulouse, France. 〈http://www.erts2016.org/〉. 〈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. ACM, 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. 〈http://dl.acm.org/citation.cfm?id=2676724〉. 〈hal-01101937〉
Accès au bibtex
BibTex

2014

Conference papers

ref_biblio
Xavier Leroy. Compiler verification for fun and profit. Koen Claessen and Viktor Kuncak. FMCAD 2014 - Formal Methods in Computer-Aided Design, Oct 2014, Lausanne, Switzerland. FMCAD Inc, 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. 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〉
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. Springer, 8558, pp.543-548, 2014, Lecture Notes in Computer Science. 〈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. 2014. 〈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, Apr 2014, Paris, France. 2014. 〈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. 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〉
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. 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. 〈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. 7705, pp.386-388, 2012, Lecture Notes in Computer Science. 〈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. Springer, 7211, pp.397-416, Lecture Notes in Computer Science. 〈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, Feb 2012, Toulouse, France. 2012. 〈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, Jan 2012, Philadelphia, PA, United States. pp.521-532, 2012, 〈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. IEEE, 〈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. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, 18, pp.59-68, 2011, OpenAccess Series in Informatics. 〈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. ACM, 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, Jan 2011, Austin, TX, United States. ACM Press, pp.67-79, 2011, 〈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, 〈https://interstices.info/jcms/n_52365/comment-faire-confiance-a-un-compilateur〉. 〈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. Springer, 6011, pp.224-243, 2010, Lecture Notes in Computer Science. 〈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. ACM. 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. 2010, 〈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. ACM, pp.316-326, 2009, 〈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
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
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

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), Jan 2008, San Francisco, United States. ACM Press, pp.17-27, 2008, 〈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. Springer, 4790, pp.211-225, 2007, Lecture Notes in Artificial Intelligence. 〈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. ACM, pp.199-208, 2006, 〈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. 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. 〈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. Elsevier, 174/5, pp.95-108, 2006, Electronic Notes in Theoretical Computer Science. 〈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.. Olivier Berger. Apr 2006, Porto Alegre, Brazil. Brazilian Computer Society, pp.199-207, 2006. 〈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. EASST, pp.7-20, 2006, EASST Newsletter, volume 12. 〈hal-00154188〉
Accès au bibtex
BibTex
ref_biblio
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. 〈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. ACM Press, pp.42--54, 2006, 〈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. 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. 〈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. 2005. 〈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. Springer, 3839, pp.66-81, 2006, Lecture Notes in Computer Science. 〈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. Springer, 2986, pp.64-78, 2004, Lecture Notes in Computer Science. 〈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, 2003, 〈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. ACM, pp.160--171, 2003, 〈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 , Oct 2002, Pittsburgh, United States. ACM, 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. Springer, 2305, pp.207-236, 2002, Lecture Notes in Computer Science. 〈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. Isabelle Attali; Thomas Jensen. Smart card programming and security, proceedings E-Smart 2001, Sep 2001, Cannes, France. Springer, 2149, pp.150-164, LNCS. 〈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. Gérard Berry; Hubert Comon; Alain Finkel. Computer Aided Verification, CAV 2001, Jul 2001, Paris, France. Springer, 2102, pp.265-285, LNCS. 〈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, 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
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

1999

Conference papers

ref_biblio
François Pessaux, Xavier Leroy. Type-based analysis of uncaught exceptions. POPL 1999: 26th symposium Principles of Programming Languages, Jan 1999, San Antonio, United States. ACM, pp.276 - 290, 1999, 〈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, 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. Springer, 1473, pp.1-8, LNCS. 〈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. ACM, 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, Jan 1995, San Francisco, United States. ACM, pp.142 - 153, 1995, 〈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. 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
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

1994

Conference papers

ref_biblio
Xavier Leroy. Manifest types, modules, and separate compilation. POPL 1994: 21st symposium Principles of Programming Languages, Jan 1994, Portland, United States. ACM, pp.109-122, 1994, 〈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. ACM, pp.220-231, 1993, 〈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, 1993, 〈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. ACM, pp.177-188, 1992, 〈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. John Hughes. FPCA 1991: Functional Programming Languages and Computer Architecture, Aug 1991, Boston, United States. Springer, 523, pp.406-426, LNCS. 〈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, Jan 1991, Orlando, United States. ACM, pp.291-302, 1991, 〈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. Pierre Deransart; Jan Maluszynski. PLILP 1990: Programming Language Implementation and Logic Programming, Aug 1990, Linköping, Sweden. Springer, 456, LNCS. 〈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, Apr 1990, Tiberias, Israel. North-Holland, 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