|
[1]
|
Andrew W. Appel and Xavier Leroy.
Efficient extensional binary tries.
Journal of Automated Reasoning, 67:article 8, 2023.
|
|
[2]
|
Xavier Leroy.
The CompCert verified compiler, software and commented proof.
Available at https://compcert.org/, November 2022.
|
|
[3]
|
Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael
Schmidt, and Simon Wegener.
Embedded program annotations for WCET analysis.
In WCET 2018: 18th International Workshop on Worst-Case
Execution Time Analysis, volume 63 of OASIcs. Dagstuhl Publishing,
July 2018.
|
|
[4]
|
Daniel Kästner, Ulrich Wünsche, Jörg Barrho, Marc Schlickling, Bernhard
Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine
Blazy.
CompCert: Practical experience on integrating and qualifying a
formally verified optimizing compiler.
In ERTS 2018: Embedded Real Time Software and Systems. SEE,
January 2018.
|
|
[5]
|
Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael
Schmidt, and Christian Ferdinand.
Closing the gap -- the formally verified optimizing compiler
CompCert.
In SSS'17: Developments in System Safety Engineering:
Proceedings of the Twenty-fifth Safety-critical Systems Symposium, pages
163--180. CreateSpace, 2017.
|
|
[6]
|
Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus
Pister, and Christian Ferdinand.
CompCert -- a formally verified optimizing compiler.
In ERTS 2016: Embedded Real Time Software and Systems. SEE,
2016.
|
|
[7]
|
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond.
Verified compilation of floating-point computations.
Journal of Automated Reasoning, 54(2):135--163, 2015.
|
|
[8]
|
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond.
A formally-verified C compiler supporting floating-point
arithmetic.
In ARITH 2013: 21st International Symposium on Computer
Arithmetic, pages 107--115. IEEE Computer Society, 2013.
|
|
[9]
|
Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc
Pantel, and Jean Souyris.
Formally verified optimizing compilation in ACG-based flight
control software.
In ERTS 2012: Embedded Real Time Software and Systems, 2012.
|
|
[10]
|
Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean
Souyris.
Towards formally verified optimizing compilation in flight control
software.
In PPES 2011: Predictability and Performance in Embedded
Systems, number 18 in OASIcs, pages 59--68. Dagstuhl Publishing, 2011.
|
|
[11]
|
Silvain Rideau and Xavier Leroy.
Validating register allocation and spilling.
In CC 2010: Compiler Construction, number 6011 in LNCS, pages
224--243. Springer, 2010.
|
|
[12]
|
Xavier Leroy.
A formally verified compiler back-end.
Journal of Automated Reasoning, 43(4):363--446, 2009.
|
|
[13]
|
Xavier Leroy.
Formal verification of a realistic compiler.
Communications of the ACM, 52(7):107--115, 2009.
|
|
[14]
|
Laurence Rideau, Bernard P. Serpette, and Xavier Leroy.
Tilting at windmills with Coq: formal verification of a compilation
algorithm for parallel moves.
Journal of Automated Reasoning, 40(4):307--326, 2008.
|
|
[15]
|
Xavier Leroy.
Formal certification of a compiler back-end, or: programming a
compiler with a proof assistant.
In POPL 2006: 33rd symposium Principles of Programming
Languages, pages 42--54. ACM, 2006.
|
|
[16]
|
Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy.
Formal verification of a C compiler front-end.
In FM 2006: Int. Symp. on Formal Methods, number 4085 in LNCS,
pages 460--475. Springer, 2006.
|
|
[1]
|
Nathanaël Courant and Xavier Leroy.
Verified code generation for the polyhedral model.
Proc. ACM Program. Lang., 5(POPL):40:1--40:24, 2021.
|
|
[2]
|
Timothy Bourke, Lélio Brun, Pierre Évariste Dagand, Xavier Leroy, Marc
Pouzet, and Lionel Rieg.
A formally verified compiler for Lustre.
In PLDI 2017: Programming Language Design and Implementation,
pages 586--601. ACM, 2017.
|
|
[3]
|
Jacques-Henri Jourdan, François Pottier, and Xavier Leroy.
Validating LR(1) parsers.
In ESOP 2012: Programming Languages and Systems, 21st European
Symposium on Programming, number 7211 in LNCS, pages 397--416. Springer,
2012.
|
|
[4]
|
Valentin Robert and Xavier Leroy.
A formally-verified alias analysis.
In CPP 2012: Certified Programs and Proofs, number 7679 in
LNCS, pages 11--26. Springer, 2012.
|
|
[5]
|
Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy.
Formal verification of object layout for C++ multiple inheritance.
In POPL 2011: 38th symposium Principles of Programming
Languages, pages 67--79. ACM, 2011.
|
|
[6]
|
Xavier Leroy.
Verified squared: does critical software deserve verified tools?
In POPL 2011: 38th symposium Principles of Programming
Languages, pages 1--2, Austin, TX, USA, January 2011. ACM.
|
|
[7]
|
Xavier Leroy.
Comment faire confiance à un compilateur?
La Recherche, 440, April 2010.
|
|
[8]
|
Jean-Baptiste Tristan and Xavier Leroy.
A simple, verified validator for software pipelining.
In POPL 2010: 37th symposium Principles of Programming
Languages, pages 83--92. ACM, 2010.
|
|
[9]
|
Jean-Baptiste Tristan and Xavier Leroy.
Verified validation of Lazy Code Motion.
In PLDI 2009: Programming Language Design and Implementation,
pages 316--326. ACM, 2009.
|
|
[10]
|
Zaynah Dargaye and Xavier Leroy.
A verified framework for higher-order uncurrying optimizations.
Higher-Order and Symbolic Computation, 22(3):199--231, 2009.
|
|
[11]
|
Jean-Baptiste Tristan and Xavier Leroy.
Formal verification of translation validators: A case study on
instruction scheduling optimizations.
In POPL 2008: 35th symposium Principles of Programming
Languages, pages 17--27. ACM, 2008.
|
|
[12]
|
Zaynah Dargaye and Xavier Leroy.
Mechanized verification of CPS transformations.
In LPAR 2007: Logic for Programming, Artificial Intelligence and
Reasoning, number 4790 in LNAI, pages 211--225. Springer, 2007.
|
|
[13]
|
Yves Bertot, Benjamin Grégoire, and Xavier Leroy.
A structured approach to proving compiler optimizations based on
dataflow analysis.
In TYPES 2004: Types for Proofs and Programs, number 3839 in
LNCS, pages 66--81. Springer, 2006.
|
|
[1]
|
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart.
The CompCert memory model.
In Andrew W. Appel, editor, Program Logics for Certified
Compilers, pages 237--271. Cambridge University Press, March 2014.
|
|
[2]
|
Robbert Krebbers, Xavier Leroy, and Freek Wiedijk.
Formal C semantics: CompCert and the C standard.
In ITP 2014: Interactive Theorem Proving, number 8558 in LNCS,
pages 543--548. Springer, 2014.
|
|
[3]
|
Xavier Leroy.
Mechanized semantics for compiler verification.
In APLAS 2012: Programming Languages and Systems, 10th Asian
Symposium, number 7705 in LNCS, pages 386--388, Kyoto, Japan, December 2012.
Springer.
|
|
[4]
|
Andrew W. Appel, Robert Dockins, and Xavier Leroy.
A list-machine benchmark for mechanized metatheory.
Journal of Automated Reasoning, 49(3):453--491, 2012.
|
|
[5]
|
Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy.
A mechanized semantics for C++ object construction and destruction,
with applications to resource management.
In POPL 2012: 39th symposium Principles of Programming
Languages, pages 521--532. ACM, 2012.
|
|
[6]
|
Xavier Leroy.
Mechanized semantics.
In J. Esparza, B. Spanfelner, and O. Grumberg, editors, Logics
and languages for reliability and security, number 25 in NATO Science for
Peace and Security Series D: Information and Communication Security, pages
195--224. IOS Press, 2010.
|
|
[7]
|
Xavier Leroy and Hervé Grall.
Coinductive big-step operational semantics.
Information and Computation, 207(2):284--304, 2009.
|
|
[8]
|
Sandrine Blazy and Xavier Leroy.
Mechanized semantics for the Clight subset of the C language.
Journal of Automated Reasoning, 43(3):263--288, 2009.
|
|
[9]
|
Xavier Leroy and Sandrine Blazy.
Formal verification of a C-like memory model and its uses for
verifying program transformations.
Journal of Automated Reasoning, 41(1):1--31, 2008.
|
|
[10]
|
Andrew W. Appel and Xavier Leroy.
A list-machine benchmark for mechanized metatheory (extended
abstract).
In LFMTP 2006: Int. Workshop on Logical Frameworks and
Meta-Languages, number 174/5 in ENTCS, pages 95--108, 2007.
|
|
[11]
|
Xavier Leroy.
A locally nameless solution to the POPLmark challenge.
Research report 6098, INRIA, January 2007.
|
|
[12]
|
Xavier Leroy.
Coinductive big-step operational semantics.
In ESOP 2006: European Symposium on Programming, number 3924 in
LNCS, pages 54--68. Springer, 2006.
|
|
[13]
|
Andrew W. Appel and Xavier Leroy.
A list-machine benchmark for mechanized metatheory.
Research report 5914, INRIA, 2006.
|
|
[14]
|
Sandrine Blazy and Xavier Leroy.
Formal verification of a memory model for C-like imperative
languages.
In ICFEM 2005: International Conference on Formal Engineering
Methods, number 3785 in LNCS, pages 280--299. Springer, 2005.
|
|
[1]
|
Tom Hirschowitz and Xavier Leroy.
Mixin modules in a call-by-value setting.
ACM Transactions on Programming Languages and Systems,
27(5):857--881, 2005.
|
|
[2]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
Call-by-value mixin modules: reduction semantics, side effects,
types.
In ESOP 2004: European Symposium on Programming, number 2986 in
LNCS, pages 64--78. Springer, 2004.
|
|
[3]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
On the implementation of recursion in call-by-value functional
languages.
Research report 4728, INRIA, 2003.
|
|
[4]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
A reduction semantics for call-by-value mixin modules.
Research report 4682, INRIA, 2003.
|
|
[5]
|
Tom Hirschowitz and Xavier Leroy.
Mixin modules in a call-by-value setting.
In ESOP 2002: European Symposium on Programming, number 2305 in
LNCS, pages 6--20. Springer, 2002.
|
|
[6]
|
Xavier Leroy.
A modular module system.
Journal of Functional Programming, 10(3):269--303, 2000.
|
|
[7]
|
Xavier Leroy.
A syntactic theory of type generativity and sharing.
Journal of Functional Programming, 6(5):667--698, 1996.
|
|
[8]
|
Xavier Leroy.
Applicative functors and fully transparent higher-order modules.
In POPL 1995: 22nd symposium Principles of Programming
Languages, pages 142--153. ACM, 1995.
|
|
[9]
|
Xavier Leroy.
Manifest types, modules, and separate compilation.
In POPL 1994: 21st symposium Principles of Programming
Languages, pages 109--122. ACM, 1994.
|
|
[1]
|
Xavier Leroy.
Java bytecode verification: algorithms and formalizations.
Journal of Automated Reasoning, 30(3--4):235--269, 2003.
|
|
[2]
|
Xavier Leroy.
Computer security from a programming language and static analysis
perspective.
In ESOP 2003: Programming Languages and Systems, 12th European
Symposium on Programming, number 2618 in LNCS, pages 1--9, Warsaw, Poland,
2003. Springer.
|
|
[3]
|
Xavier Leroy.
Bytecode verification on Java smart card.
Software -- Practice & Experience, 32(4):319--340, 2002.
|
|
[4]
|
Xavier Leroy.
On-card bytecode verification for Java Card.
In E-SMART 2001: Smart card programming and security, number
2140 in LNCS, pages 150--164. Springer, 2001.
|
|
[5]
|
Xavier Leroy.
Java bytecode verification: an overview.
In CAV 2001: Computer Aided Verification, number 2102 in LNCS,
pages 265--285. Springer, 2001.
|
|
[6]
|
Xavier Leroy and François Rouaix.
Security properties of typed applets.
In J. Vitek and C. Jensen, editors, Secure Internet Programming
-- Security issues for Mobile and Distributed Objects, number 1603 in LNCS,
pages 147--182. Springer, 1999.
|
|
[7]
|
Xavier Leroy and François Rouaix.
Security properties of typed applets.
In POPL 1998: 25th symposium Principles of Programming
Languages, pages 391--403. ACM, 1998.
|
|
[1]
|
Xavier Leroy.
An overview of types in compilation.
In TIC 1998: workshop Types in Compilation, number 1473 in
LNCS, pages 1--8. Springer, March 1998.
|
|
[2]
|
Xavier Leroy.
The effectiveness of type-based unboxing.
In TIC 1997: workshop Types in Compilation. Technical report
BCCS-97-03, Boston College, Computer Science Department, June 1997.
|
|
[3]
|
Xavier Leroy.
Unboxed objects and polymorphic typing.
In POPL 1992: 19th symposium Principles of Programming
Languages, pages 177--188. ACM, 1992.
|
|
[4]
|
Xavier Leroy.
Efficient data representation in polymorphic languages.
In PLILP 1990: Programming Language Implementation and Logic
Programming, number 456 in LNCS. Springer, 1990.
|
|
[5]
|
Xavier Leroy.
Efficient data representation in polymorphic languages.
Research report 1264, INRIA, 1990.
|
|
[1]
|
Xavier Leroy.
Polymorphism by name for references and continuations.
In POPL 1993: 20th symposium Principles of Programming
Languages, pages 220--231. ACM, 1993.
|
|
[2]
|
Xavier Leroy and Michel Mauny.
Dynamics in ML.
Journal of Functional Programming, 3(4):431--463, 1993.
|
|
[3]
|
Xavier Leroy.
Polymorphic typing of an algorithmic language.
Research report 1778, INRIA, 1992.
|
|
[4]
|
Xavier Leroy.
Typage polymorphe d'un langage algorithmique.
Phd thesis (in french), Université Paris 7, 1992.
|
|
[5]
|
Xavier Leroy and Pierre Weis.
Polymorphic type inference and assignment.
In POPL 1991: 18th symposium Principles of Programming
Languages, pages 291--302. ACM, 1991.
|
|
[6]
|
Xavier Leroy and Michel Mauny.
Dynamics in ML.
In FPCA 1991: Functional Programming Languages and Computer
Architecture, number 523 in LNCS, pages 406--426. Springer, 1991.
|
|
[7]
|
Luca Cardelli and Xavier Leroy.
Abstract types and the dot notation.
In Proceedings IFIP TC2 working conference on programming
concepts and methods, pages 479--504. North-Holland, 1990.
|
|
[8]
|
Luca Cardelli and Xavier Leroy.
Abstract types and the dot notation.
Research report 56, Digital Equipment Corporation, Systems Research
Center, 1990.
|
|
[1]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
Compilation of extended recursion in call-by-value functional
languages.
Higher-Order and Symbolic Computation, 22(1):3--66, 2009.
|
|
[2]
|
Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy.
Implementing multi-stage languages using ASTs, gensym, and
reflection.
In GPCE 2003: Generative Programming and Component Engineering,
number 2830 in LNCS, pages 57--76. Springer, 2003.
|
|
[3]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
Compilation of extended recursion in call-by-value functional
languages.
In PPDP 2003: International Conference on Principles and
Practice of Declarative Programming, pages 160--171. ACM, 2003.
|
|
[4]
|
Benjamin Grégoire and Xavier Leroy.
A compiled implementation of strong reduction.
In ICFP 2002: International Conference on Functional
Programming, pages 235--246. ACM, 2002.
|
|
[5]
|
Pierre Weis and Xavier Leroy.
Le langage Caml.
Dunod, 2 edition, 1999.
|
|
[6]
|
Marco Danelutto, Roberto Di Cosmo, Xavier Leroy, and Susanna Pelagatti.
Parallel functional programming with skeletons: the OCamlP3L
experiment.
In Proceedings ACM workshop on ML and its applications. Cornell
University, 1998.
|
|
[7]
|
P. H. Hartel, M. Feeley, M. Alt, L. Augustsson, P. Baumann, M. Beemster,
E. Chailloux, C. H. Flood, W. Grieskamp, J. H. G. van Groningen, K. Hammond,
B. Hausman, M. Y. Ivory, R. E. Jones, J. Kamperman, P. Lee, X. Leroy, R. D.
Lins, S. Loosemore, N. Röjemo, M. Serrano, J.-P. Talpin, J. Thackray,
S. Thomas, P. Walters, P. Weis, and P. Wentworth.
Benchmarking implementations of functional languages with
“Pseudoknot”, a float-intensive benchmark.
Journal of Functional Programming, 6(4):621--655, 1996.
|
|
[8]
|
Xavier Leroy.
Le système Caml Special Light: modules et compilation
efficace en Caml.
In Actes des Journées Francophones des Langages Applicatifs,
pages 111--131. INRIA, January 1996.
|
|
[9]
|
Xavier Leroy.
Le système Caml Special Light: modules et compilation
efficace en Caml.
Research report 2721, INRIA, November 1995.
|
|
[10]
|
Xavier Leroy and Pierre Weis.
Manuel de référence du langage Caml.
InterÉditions, 1993.
|
|
[11]
|
Damien Doligez and Xavier Leroy.
A concurrent, generational garbage collector for a multithreaded
implementation of ML.
In POPL 1993: 20th symposium Principles of Programming
Languages, pages 113--123. ACM, 1993.
|
|
[12]
|
Xavier Leroy.
Programmation du système Unix en Caml Light.
Technical report 147, INRIA, 1992.
|
|
[13]
|
Xavier Leroy.
The ZINC experiment: an economical implementation of the ML
language.
Technical report 117, INRIA, 1990.
|
|
[1]
|
Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, and Jérôme
Vouillon.
Maintaining large software distributions: new challenges from the
FOSS era.
In FRCSS 2006: Future Research Challenges for Software and
Services, number 12 in EASST Newsletter, pages 7--20, 2006.
|
|
[2]
|
Fabio Mancinelli, Roberto Di Cosmo, Jérôme Vouillon, Jaap Boender, Berke
Durak, Xavier Leroy, and Ralf Treinen.
Managing the complexity of large free and open source package-based
software distributions.
In ASE 2006: 21st Int. Conf. on Automated Software Engineering,
pages 199--208. IEEE Computer Society, 2006.
|
|
[3]
|
Serge Abiteboul, Ciarán Bryce, Roberto Di Cosmo, Klaus R. Dittrich, Stéfane
Fermigier, Stéphane Laurière, Frédéric Lepied, Xavier Leroy, Tova Milo,
Eleonora Panto, Radu Pop, Assaf Sagi, Yotam Shtossel, Florent Villard, and
Boris Vrdoljak.
EDOS: Environment for the Development and Distribution of
Open Source Software.
In OSS 2005: International Conference on Open Source
Systems, 2005.
|