|
[1]
|
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond.
A formally-verified C compiler supporting floating-point
arithmetic.
In ARITH, 21st IEEE International Symposium on Computer
Arithmetic, pages 107-115. IEEE Computer Society Press, 2013.
|
|
[2]
|
Xavier Leroy.
The CompCert verified compiler, software and commented proof.
Available at http://compcert.inria.fr/, January 2013.
|
|
[3]
|
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart.
The CompCert memory model, version 2.
Research report RR-7987, INRIA, June 2012.
|
|
[4]
|
Valentin Robert and Xavier Leroy.
A formally-verified alias analysis.
In Certified Programs and Proofs (CPP 2012), volume 7679 of
Lecture Notes in Computer Science, pages 11-26. Springer, 2012.
|
|
[5]
|
Jacques-Henri Jourdan, François Pottier, and Xavier Leroy.
Validating LR(1) parsers.
In Programming Languages and Systems - 21st European Symposium
on Programming, ESOP 2012, volume 7211 of Lecture Notes in Computer
Science, pages 397-416. Springer, 2012.
|
|
[6]
|
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 Embedded Real Time Software and Systems (ERTS 2012), 2012.
|
|
[7]
|
Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean
Souyris.
Towards formally verified optimizing compilation in flight control
software.
In Bringing Theory to Practice: Predictability and Performance
in Embedded Systems (PPES 2011), volume 18 of OpenAccess Series in
Informatics (OASIcs), pages 59-68. Schloss Dagstuhl-Leibniz-Zentrum fuer
Informatik, 2011.
|
|
[8]
|
Xavier Leroy.
Verified squared: does critical software deserve verified tools?
In 38th symposium Principles of Programming Languages, pages
1-2. ACM Press, 2011.
Abstract of invited lecture.
|
|
[9]
|
Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy.
Formal verification of object layout for C++ multiple inheritance.
In 38th symposium Principles of Programming Languages, pages
67-79. ACM Press, 2011.
|
|
[10]
|
Xavier Leroy.
Comment faire confiance à un compilateur?
La Recherche, 440, April 2010.
Les cahiers de l'INRIA.
|
|
[11]
|
Silvain Rideau and Xavier Leroy.
Validating register allocation and spilling.
In Compiler Construction (CC 2010), volume 6011 of Lecture
Notes in Computer Science, pages 224-243. Springer, 2010.
|
|
[12]
|
Jean-Baptiste Tristan and Xavier Leroy.
A simple, verified validator for software pipelining.
In 37th symposium Principles of Programming Languages, pages
83-92. ACM Press, 2010.
|
|
[13]
|
Xavier Leroy.
Formal verification of a realistic compiler.
Communications of the ACM, 52(7):107-115, 2009.
|
|
[14]
|
Zaynah Dargaye and Xavier Leroy.
A verified framework for higher-order uncurrying optimizations.
Higher-Order and Symbolic Computation, 22(3):199-231, 2009.
|
|
[15]
|
Jean-Baptiste Tristan and Xavier Leroy.
Verified validation of Lazy Code Motion.
In Programming Language Design and Implementation 2009, pages
316-326. ACM Press, 2009.
|
|
[16]
|
Xavier Leroy.
A formally verified compiler back-end.
Journal of Automated Reasoning, 43(4):363-446, 2009.
|
|
[17]
|
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.
|
|
[18]
|
Jean-Baptiste Tristan and Xavier Leroy.
Formal verification of translation validators: A case study on
instruction scheduling optimizations.
In 35th symposium Principles of Programming Languages, pages
17-27. ACM Press, 2008.
|
|
[19]
|
Zaynah Dargaye and Xavier Leroy.
Mechanized verification of CPS transformations.
In Logic for Programming, Artificial Intelligence and Reasoning,
14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial
Intelligence, pages 211-225. Springer, 2007.
|
|
[20]
|
Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy.
Formal verification of a C compiler front-end.
In FM 2006: Int. Symp. on Formal Methods, volume 4085 of
Lecture Notes in Computer Science, pages 460-475. Springer, 2006.
|
|
[21]
|
Xavier Leroy.
Formal certification of a compiler back-end, or: programming a
compiler with a proof assistant.
In 33rd symposium Principles of Programming Languages, pages
42-54. ACM Press, 2006.
|
|
[22]
|
Yves Bertot, Benjamin Grégoire, and Xavier Leroy.
A structured approach to proving compiler optimizations based on
dataflow analysis.
In Types for Proofs and Programs, Workshop TYPES 2004, volume
3839 of Lecture Notes in Computer Science, pages 66-81. Springer,
2006.
|
|
[1]
|
Xavier Leroy.
Mechanized semantics for compiler verification.
In Ranjit Jhala and Atsushi Igarashi, editors, Programming
Languages and Systems, 10th Asian Symposium, APLAS 2012, volume 7705 of
Lecture Notes in Computer Science, pages 386-388. Springer, 2012.
Abstract of invited talk.
|
|
[2]
|
Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy.
A mechanized semantics for C++ object construction and destruction,
with applications to resource management.
In 39th symposium Principles of Programming Languages, pages
521-532. ACM Press, 2012.
|
|
[3]
|
Andrew W. Appel, Robert Dockins, and Xavier Leroy.
A list-machine benchmark for mechanized metatheory.
Journal of Automated Reasoning, 49(3):453-491, 2012.
|
|
[4]
|
Xavier Leroy.
Mechanized semantics.
In Logics and languages for reliability and security, volume 25
of NATO Science for Peace and Security Series D: Information and
Communication Security, pages 195-224. IOS Press, 2010.
|
|
[5]
|
Sandrine Blazy and Xavier Leroy.
Mechanized semantics for the Clight subset of the C language.
Journal of Automated Reasoning, 43(3):263-288, 2009.
|
|
[6]
|
Xavier Leroy and Hervé Grall.
Coinductive big-step operational semantics.
Information and Computation, 207(2):284-304, 2009.
|
|
[7]
|
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.
|
|
[8]
|
Xavier Leroy.
A locally nameless solution to the POPLmark challenge.
Research report 6098, INRIA, January 2007.
|
|
[9]
|
Andrew W. Appel and Xavier Leroy.
A list-machine benchmark for mechanized metatheory (extended
abstract).
In Proc. Int. Workshop on Logical Frameworks and Meta-Languages
(LFMTP'06), volume 174/5 of Electronic Notes in Theoretical Computer
Science, pages 95-108, 2007.
|
|
[10]
|
Andrew W. Appel and Xavier Leroy.
A list-machine benchmark for mechanized metatheory.
Research report 5914, INRIA, 2006.
|
|
[11]
|
Xavier Leroy.
Coinductive big-step operational semantics.
In European Symposium on Programming (ESOP 2006), volume 3924
of Lecture Notes in Computer Science, pages 54-68. Springer, 2006.
|
|
[12]
|
Sandrine Blazy and Xavier Leroy.
Formal verification of a memory model for C-like imperative
languages.
In International Conference on Formal Engineering Methods (ICFEM
2005), volume 3785 of Lecture Notes in Computer Science, 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 European Symposium on Programming, volume 2986 of
Lecture Notes in Computer Science, pages 64-78. Springer, 2004.
|
|
[3]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
A reduction semantics for call-by-value mixin modules.
Research report 4682, INRIA, 2003.
|
|
[4]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
On the implementation of recursion in call-by-value functional
languages.
Research report 4728, INRIA, 2003.
|
|
[5]
|
Tom Hirschowitz and Xavier Leroy.
Mixin modules in a call-by-value setting.
In D. Le Métayer, editor, Programming Languages and Systems,
ESOP'2002, volume 2305 of Lecture Notes in Computer Science, 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 22nd symposium Principles of Programming Languages, pages
142-153. ACM Press, 1995.
|
|
[9]
|
Xavier Leroy.
Manifest types, modules, and separate compilation.
In 21st symposium Principles of Programming Languages, pages
109-122. ACM Press, 1994.
|
|
[1]
|
Xavier Leroy.
Computer security from a programming language and static analysis
perspective.
In P. Degano, editor, Programming Languages and Systems: 12th
European Symposium on Programming, ESOP 2003, volume 2618 of Lecture
Notes in Computer Science, pages 1-9. Springer, 2003.
Abstract of invited lecture.
|
|
[2]
|
Xavier Leroy.
Java bytecode verification: algorithms and formalizations.
Journal of Automated Reasoning, 30(3-4):235-269, 2003.
|
|
[3]
|
Xavier Leroy.
Bytecode verification for Java smart card.
Software - Practice & Experience, 32(4):319-340, 2002.
|
|
[4]
|
Xavier Leroy.
Java bytecode verification: an overview.
In G. Berry, H. Comon, and A. Finkel, editors, Computer Aided
Verification, CAV 2001, volume 2102 of Lecture Notes in Computer
Science, pages 265-285. Springer, 2001.
|
|
[5]
|
Xavier Leroy.
On-card bytecode verification for Java card.
In I. Attali and T. Jensen, editors, Smart card programming and
security, proceedings E-Smart 2001, volume 2140 of Lecture Notes in
Computer Science, pages 150-164. 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, volume 1603 of
Lecture Notes in Computer Science, pages 147-182. Springer, 1999.
|
|
[7]
|
Xavier Leroy and François Rouaix.
Security properties of typed applets.
In 25th symposium Principles of Programming Languages, pages
391-403. ACM Press, 1998.
|
|
[1]
|
François Pessaux and Xavier Leroy.
Type-based analysis of uncaught exceptions.
ACM Transactions on Programming Languages and Systems,
22(2):340-377, 2000.
|
|
[2]
|
François Pessaux and Xavier Leroy.
Type-based analysis of uncaught exceptions.
In 26th symposium Principles of Programming Languages, pages
276-290. ACM Press, 1999.
|
|
[3]
|
Xavier Leroy.
Introduction to types in compilation.
In Proceedings of the 1998 Types in Compilation workshop,
volume 1473 of Lecture Notes in Computer Science, pages 1-8. Springer,
March 1998.
|
|
[4]
|
Xavier Leroy.
The effectiveness of type-based unboxing.
In Workshop Types in Compilation '97. Technical report
BCCS-97-03, Boston College, Computer Science Department, June 1997.
|
|
[5]
|
Xavier Leroy.
Unboxed objects and polymorphic typing.
In 19th symposium Principles of Programming Languages, pages
177-188. ACM Press, 1992.
|
|
[6]
|
Xavier Leroy.
Efficient data representation in polymorphic languages.
Research report 1264, INRIA, 1990.
|
|
[7]
|
Xavier Leroy.
Efficient data representation in polymorphic languages.
In P. Deransart and J. Maluszyński, editors, Programming
Language Implementation and Logic Programming 90, volume 456 of Lecture
Notes in Computer Science. Springer, 1990.
|
|
[1]
|
Xavier Leroy and Michel Mauny.
Dynamics in ML.
Journal of Functional Programming, 3(4):431-463, 1993.
|
|
[2]
|
Xavier Leroy.
Polymorphism by name for references and continuations.
In 20th symposium Principles of Programming Languages, pages
220-231. ACM Press, 1993.
|
|
[3]
|
Xavier Leroy.
Typage polymorphe d'un langage algorithmique.
Phd thesis (in french), Université Paris 7, 1992.
|
|
[4]
|
Xavier Leroy.
Polymorphic typing of an algorithmic language.
Research report 1778, INRIA, 1992.
|
|
[5]
|
Xavier Leroy and Michel Mauny.
Dynamics in ML.
In John Hughes, editor, Functional Programming Languages and
Computer Architecture 1991, volume 523 of Lecture Notes in Computer
Science, pages 406-426. Springer, 1991.
|
|
[6]
|
Xavier Leroy and Pierre Weis.
Polymorphic type inference and assignment.
In 18th symposium Principles of Programming Languages, pages
291-302. ACM Press, 1991.
|
|
[7]
|
Luca Cardelli and Xavier Leroy.
Abstract types and the dot notation.
Research report 56, Digital Equipment Corporation, Systems Research
Center, 1990.
|
|
[8]
|
Luca Cardelli and Xavier Leroy.
Abstract types and the dot notation.
In M. Broy and C. B. Jones, editors, Proceedings IFIP TC2
working conference on programming concepts and methods, pages 479-504.
North-Holland, 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]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
Compilation of extended recursion in call-by-value functional
languages.
In International Conference on Principles and Practice of
Declarative Programming, pages 160-171. ACM Press, 2003.
|
|
[3]
|
Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy.
Implementing multi-stage languages using ASTs, gensym, and
reflection.
In Generative Programming and Component Engineering, 2nd Int.
Conf. GPCE 2003, volume 2830 of Lecture Notes in Computer Science,
pages 57-76. Springer, 2003.
|
|
[4]
|
Benjamin Grégoire and Xavier Leroy.
A compiled implementation of strong reduction.
In International Conference on Functional Programming 2002,
pages 235-246. ACM Press, 2002.
|
|
[5]
|
Pierre Weis and Xavier Leroy.
Le langage Caml.
Dunod, 1999.
|
|
[6]
|
Marco Danelutto, Roberto DiCosmo, 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]
|
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.
|
|
[8]
|
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.
|
|
[9]
|
Xavier Leroy.
Le système Caml Special Light: modules et compilation
efficace en Caml.
Research report 2721, INRIA, November 1995.
|
|
[10]
|
Damien Doligez and Xavier Leroy.
A concurrent, generational garbage collector for a multithreaded
implementation of ML.
In 20th symposium Principles of Programming Languages, pages
113-123. ACM Press, 1993.
|
|
[11]
|
Xavier Leroy and Pierre Weis.
Manuel de référence du langage Caml.
InterÉditions, 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]
|
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 21st IEEE Int. Conf. on Automated Software Engineering (ASE
2006), pages 199-208. IEEE Computer Society Press, 2006.
|
|
[2]
|
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 Proceedings of the FRCSS 2006 workshop, volume 12 of
EASST Newsletter, pages 7-20, 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 First International Conference on Open Source Systems
(OSS 2005), 2005.
|