Xavier Leroy

According to our database, Xavier Leroy authored at least 75 papers between 1990 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

Efficient Extensional Binary Tries.

Andrew W. Appel, Xavier Leroy

J. Autom. Reason., March, 2023

2021

Verified code generation for the polyhedral model.

Nathanaël Courant, Xavier Leroy

Proc. ACM Program. Lang., 2021

2018

Embedded Program Annotations for WCET Analysis.

Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, Simon Wegener

Proceedings of the 18th International Workshop on Worst-Case Execution Time Analysis, 2018

2017

A formally verified compiler for Lustre.

Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

2016

Formally Verifying a Compiler: What Does It Mean, Exactly?

Xavier Leroy

Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

2015

Verified Compilation of Floating-Point Computations.

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond

J. Autom. Reason., 2015

A Formally-Verified C Static Analyzer.

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2014

Formal Proofs of Code Generation and Verification Tools.

Xavier Leroy

Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Formal C Semantics: CompCert and the C Standard.

Robbert Krebbers, Xavier Leroy, Freek Wiedijk

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Compiler verification for fun and profit.

Xavier Leroy

Proceedings of the Formal Methods in Computer-Aided Design, 2014

2013

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic.

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond

Proceedings of the 21st IEEE Symposium on Computer Arithmetic, 2013

2012

A List-Machine Benchmark for Mechanized Metatheory.

Andrew W. Appel, Robert Dockins, Xavier Leroy

J. Autom. Reason., 2012

A mechanized semantics for C++ object construction and destruction, with applications to resource management.

Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Validating LR(1) Parsers.

Jacques-Henri Jourdan, François Pottier, Xavier Leroy

Proceedings of the Programming Languages and Systems, 2012

A Formally-Verified Alias Analysis.

Valentin Robert, Xavier Leroy

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

Mechanized Semantics for Compiler Verification.

Xavier Leroy

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011

Special Issue Dedicated to ICFP 2009 Editorial.

Andrew P. Tolmach, Xavier Leroy

J. Funct. Program., 2011

Safety first!: technical perspective.

Xavier Leroy

Commun. ACM, 2011

Formal verification of object layout for c++ multiple inheritance.

Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Verified squared: does critical software deserve verified tools?

Xavier Leroy

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Towards Formally Verified Optimizing Compilation in Flight Control Software.

Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris

Proceedings of the Bringing Theory to Practice: Predictability and Performance in Embedded Systems, 2011

Formally verifying a compiler: Why? How? How far?

Xavier Leroy

Proceedings of the CGO 2011, 2011

2010

Mechanized semantics - with applications to program proof and compiler verification.

Xavier Leroy

Proceedings of the Logics and Languages for Reliability and Security, 2010

Mechanized semantics

Xavier Leroy

CoRR, 2010

A simple, verified validator for software pipelining.

Jean-Baptiste Tristan, Xavier Leroy

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Validating Register Allocation and Spilling.

Silvain Rideau, Xavier Leroy

Proceedings of the Compiler Construction, 19th International Conference, 2010

2009

Compilation of extended recursion in call-by-value functional languages.

Tom Hirschowitz, Xavier Leroy, J. B. Wells

High. Order Symb. Comput., 2009

A verified framework for higher-order uncurrying optimizations.

Zaynah Dargaye, Xavier Leroy

High. Order Symb. Comput., 2009

Editorial.

Xavier Leroy, Matthias Felleisen

J. Funct. Program., 2009

Editorial.

Xavier Leroy

J. Funct. Program., 2009

A Formally Verified Compiler Back-end.

Xavier Leroy

J. Autom. Reason., 2009

Mechanized Semantics for the Clight Subset of the C Language.

Sandrine Blazy, Xavier Leroy

J. Autom. Reason., 2009

Coinductive big-step operational semantics.

Xavier Leroy, Hervé Grall

Inf. Comput., 2009

Formal verification of a realistic compiler.

Xavier Leroy

Commun. ACM, 2009

Verified validation of lazy code motion.

Jean-Baptiste Tristan, Xavier Leroy

Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

2008

Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves.

Laurence Rideau, Bernard P. Serpette, Xavier Leroy

J. Autom. Reason., 2008

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations.

Xavier Leroy, Sandrine Blazy

J. Autom. Reason., 2008

Formal verification of translation validators: a case study on instruction scheduling optimizations.

Jean-Baptiste Tristan, Xavier Leroy

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

2007

Formal verification of an optimizing compiler.

Xavier Leroy

Proceedings of the 5th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2007), May 30, 2007

Mechanized Verification of CPS Transformations.

Zaynah Dargaye, Xavier Leroy

Proceedings of the Logic for Programming, 2007

2006

A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract).

Andrew W. Appel, Xavier Leroy

Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2006

Formal certification of a compiler back-end or: programming a compiler with a proof assistant.

Xavier Leroy

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

Managing the Complexity of Large Free and Open Source Package-Based Software Distributions.

Fabio Mancinelli, Jaap Boender, Roberto Di Cosmo, Jerome Vouillon, Berke Durak, Xavier Leroy, Ralf Treinen

Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), 2006

Formal Verification of a C Compiler Front-End.

Sandrine Blazy, Zaynah Dargaye, Xavier Leroy

Proceedings of the FM 2006: Formal Methods, 2006

Coinductive Big-Step Operational Semantics.

Xavier Leroy

Proceedings of the Programming Languages and Systems, 2006

2005

Mixin modules in a call-by-value setting.

Tom Hirschowitz, Xavier Leroy

ACM Trans. Program. Lang. Syst., 2005

Preface.

Nick Benton, Xavier Leroy

Proceedings of the ACM-SIGPLAN Workshop on ML, 2005

Formal Verification of a Memory Model for <i>C</i>-Like Imperative Languages.

Sandrine Blazy, Xavier Leroy

Proceedings of the Formal Methods and Software Engineering, 2005

2004

A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.

Yves Bertot, Benjamin Grégoire, Xavier Leroy

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types.

Tom Hirschowitz, Xavier Leroy, J. B. Wells

Proceedings of the Programming Languages and Systems, 2004

2003

Java Bytecode Verification: Algorithms and Formalizations.

Xavier Leroy

J. Autom. Reason., 2003

Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection.

Cristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy

Proceedings of the Generative Programming and Component Engineering, 2003

Computer Security from a Programming Language and Static Analysis Perspective.

Xavier Leroy

Proceedings of the Programming Languages and Systems, 2003

2002

Bytecode verification on Java smart cards.

Xavier Leroy

Softw. Pract. Exp., 2002

A compiled implementation of strong reduction.

Benjamin Grégoire, Xavier Leroy

Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), 2002

2001

On-Card Bytecode Verification for Java Card.

Xavier Leroy

Proceedings of the Smart Card Programming and Security, 2001

Java Bytecode Verification: An Overview.

Xavier Leroy

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Type-based analysis of uncaught exceptions.

Xavier Leroy, François Pessaux

ACM Trans. Program. Lang. Syst., 2000

A modular module system.

Xavier Leroy

J. Funct. Program., 2000

1998

Introduction.

Xavier Leroy

Proceedings of the Types in Compilation, Second International Workshop, 1998

Security Properties of Typed Applets.

Xavier Leroy, François Rouaix

Proceedings of the POPL '98, 1998

1996

A Syntactic Theory of Type Generativity and Sharing.

Xavier Leroy

J. Funct. Program., 1996

Benchmarking Implementations of Functional Languages with 'Pseudoknot', a Float-Intensive Benchmark.

Pieter H. Hartel, Marc Feeley, Martin Helmut Alt, Lennart Augustsson, Peter Baumann, Marcel Beemster, Emmanuel Chailloux, Christine H. Flood, Wolfgang Grieskamp, John H. G. van Groningen, Kevin Hammond, Bogumil Hausman, Melody Y. Ivory, Richard E. Jones, Jasper Kamperman, Peter Lee, Xavier Leroy, Rafael Dueire Lins, Sandra Loosemore, Niklas Röjemo, Manuel Serrano, Jean-Pierre Talpin, Jon Thackray, Stephen Thomas, Pum Walters, Pierre Weis, Peter Wentworth

J. Funct. Program., 1996

1995

Applicative Functors and Fully Transparent Higher-Order Modules.

Xavier Leroy

Proceedings of the Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995

1994

Manifest Types, Modules, and Separate Compilation.

Xavier Leroy

Proceedings of the Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994

1993

Dynamics in ML.

Xavier Leroy, Michel Mauny

J. Funct. Program., 1993

Polymorphism by Name for References and Continuations.

Xavier Leroy

Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML.

Damien Doligez, Xavier Leroy

Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

Manuel de référence du langage CAML.

Xavier Leroy, Pierre Weis

InterEditions, ISBN: 978-2-7296-0492-9, 1993

Le langage Caml.

Pierre Weis, Xavier Leroy

InterEditions, ISBN: 978-2-7296-0493-6, 1993

1992

Typage polymorphe d'un langage algorithmique. (Polymorphic typing of an algorithmic language).

Xavier Leroy

PhD thesis, 1992

Unboxed Objects and Polymorphic Typing.

Xavier Leroy

Proceedings of the Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1992

1991

Polymorphic Type Inference and Assignment.

Xavier Leroy, Pierre Weis

Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991

1990

Efficient Data Representation in Polymorphic Languages.

Xavier Leroy

Proceedings of the Programming Language Implementation and Logic Programming, 1990

Abstract Types and the Dot Notation.

Luca Cardelli, Xavier Leroy

Proceedings of the Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 1990