Xavier Leroy

ORCID

Publication Activity (10 Years)

Years Active: 1990-2023
Publications (10 Years): 6

Top Venues

J. Autom. Reason.

Proc. ACM Program. Lang.

ITP

CoRR

Paris Diderot University, France (PHD)

Education History

Paris Diderot University, France

PHD

Publications

Andrew W. Appel, Xavier Leroy
Efficient Extensional Binary Tries. J. Autom. Reason. 67 (1) (2023)
Nathanaël Courant, Xavier Leroy
Verified code generation for the polyhedral model. Proc. ACM Program. Lang. 5 (POPL) (2021)
Andrew W. Appel, Xavier Leroy
Efficient Extensional Binary Tries. CoRR (2021)
Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, Simon Wegener
Embedded Program Annotations for WCET Analysis. WCET (2018)
Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg
A formally verified compiler for Lustre. PLDI (2017)
Xavier Leroy
Formally Verifying a Compiler: What Does It Mean, Exactly? ICALP (2016)
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
A Formally-Verified C Static Analyzer. POPL (2015)
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
Verified Compilation of Floating-Point Computations. J. Autom. Reason. 54 (2) (2015)
Xavier Leroy
Compiler verification for fun and profit. FMCAD (2014)
Robbert Krebbers, Xavier Leroy, Freek Wiedijk
Formal C Semantics: CompCert and the C Standard. ITP (2014)
Xavier Leroy
Formal Proofs of Code Generation and Verification Tools. SEFM (2014)
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic (2013)
Xavier Leroy
Mechanized Semantics for Compiler Verification. APLAS (2012)
Andrew W. Appel, Robert Dockins, Xavier Leroy
A List-Machine Benchmark for Mechanized Metatheory. J. Autom. Reason. 49 (3) (2012)
Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy
A mechanized semantics for C++ object construction and destruction, with applications to resource management. POPL (2012)
Xavier Leroy
Mechanized Semantics for Compiler Verification. CPP (2012)
Jacques-Henri Jourdan, François Pottier, Xavier Leroy
Validating LR(1) Parsers. ESOP (2012)
Valentin Robert, Xavier Leroy
A Formally-Verified Alias Analysis. CPP (2012)
Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris
Towards Formally Verified Optimizing Compilation in Flight Control Software. PPES (2011)
Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy
Formal verification of object layout for c++ multiple inheritance. POPL (2011)
Andrew P. Tolmach, Xavier Leroy
Special Issue Dedicated to ICFP 2009 Editorial. J. Funct. Program. 21 (4-5) (2011)
Xavier Leroy
Safety first!: technical perspective. Commun. ACM 54 (12) (2011)
Xavier Leroy
Formally verifying a compiler: Why? How? How far? CGO (2011)
Xavier Leroy
Verified squared: does critical software deserve verified tools? POPL (2011)
Silvain Rideau, Xavier Leroy
Validating Register Allocation and Spilling. CC (2010)
Xavier Leroy
Mechanized semantics CoRR (2010)
Jean-Baptiste Tristan, Xavier Leroy
A simple, verified validator for software pipelining. POPL (2010)
Xavier Leroy, Hervé Grall
Coinductive big-step operational semantics. Inf. Comput. 207 (2) (2009)
Zaynah Dargaye, Xavier Leroy
A verified framework for higher-order uncurrying optimizations. High. Order Symb. Comput. 22 (3) (2009)
Xavier Leroy
Editorial. J. Funct. Program. 19 (2) (2009)
Xavier Leroy
Formal verification of a realistic compiler. Commun. ACM 52 (7) (2009)
Xavier Leroy
A Formally Verified Compiler Back-end. J. Autom. Reason. 43 (4) (2009)
Xavier Leroy, Matthias Felleisen
Editorial. J. Funct. Program. 19 (5) (2009)
Xavier Leroy
A formally verified compiler back-end CoRR (2009)
Tom Hirschowitz, Xavier Leroy, J. B. Wells
Compilation of extended recursion in call-by-value functional languages. High. Order Symb. Comput. 22 (1) (2009)
Sandrine Blazy, Xavier Leroy
Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reason. 43 (3) (2009)
Sandrine Blazy, Xavier Leroy
Mechanized semantics for the Clight subset of the C language CoRR (2009)
Jean-Baptiste Tristan, Xavier Leroy
Verified validation of lazy code motion. PLDI (2009)
Tom Hirschowitz, Xavier Leroy, J. B. Wells
Compilation of extended recursion in call-by-value functional languages CoRR (2009)
Jean-Baptiste Tristan, Xavier Leroy
Formal verification of translation validators: a case study on instruction scheduling optimizations. POPL (2008)
Xavier Leroy, Hervé Grall
Coinductive big-step operational semantics CoRR (2008)
Xavier Leroy, Sandrine Blazy
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reason. 41 (1) (2008)
Laurence Rideau, Bernard P. Serpette, Xavier Leroy
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves. J. Autom. Reason. 40 (4) (2008)
Andrew W. Appel, Xavier Leroy
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). Electron. Notes Theor. Comput. Sci. 174 (5) (2007)
Xavier Leroy
Formal verification of an optimizing compiler. MEMOCODE (2007)
Zaynah Dargaye, Xavier Leroy
Mechanized Verification of CPS Transformations. LPAR (2007)
Xavier Leroy
Formal Verification of an Optimizing Compiler. RTA (2007)
Xavier Leroy
Coinductive Big-Step Operational Semantics. ESOP (2006)
Nick Benton, Xavier Leroy
Preface. Electron. Notes Theor. Comput. Sci. 148 (2) (2006)
Xavier Leroy
Formal certification of a compiler back-end or: programming a compiler with a proof assistant. POPL (2006)
Sandrine Blazy, Zaynah Dargaye, Xavier Leroy
Formal Verification of a C Compiler Front-End. FM (2006)
Fabio Mancinelli, Jaap Boender, Roberto Di Cosmo, Jerome Vouillon, Berke Durak, Xavier Leroy, Ralf Treinen
Managing the Complexity of Large Free and Open Source Package-Based Software Distributions. ASE (2006)
Tom Hirschowitz, Xavier Leroy
Mixin modules in a call-by-value setting. ACM Trans. Program. Lang. Syst. 27 (5) (2005)
Sandrine Blazy, Xavier Leroy
-Like Imperative Languages. ICFEM (2005)
Yves Bertot, Benjamin Grégoire, Xavier Leroy
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES (2004)
Tom Hirschowitz, Xavier Leroy, J. B. Wells
Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types. ESOP (2004)
Tom Hirschowitz, Xavier Leroy, J. B. Wells
Compilation of extended recursion in call-by-value functional languages. PPDP (2003)
Xavier Leroy
Computer Security from a Programming Language and Static Analysis Perspective. ESOP (2003)
Xavier Leroy
Java Bytecode Verification: Algorithms and Formalizations. J. Autom. Reason. 30 (3-4) (2003)
Cristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. GPCE (2003)
Tom Hirschowitz, Xavier Leroy
Mixin Modules in a Call-by-Value Setting. ESOP (2002)
Benjamin Grégoire, Xavier Leroy
A compiled implementation of strong reduction. ICFP (2002)
Xavier Leroy
Bytecode verification on Java smart cards. Softw. Pract. Exp. 32 (4) (2002)
Xavier Leroy
Java Bytecode Verification: An Overview. CAV (2001)
Xavier Leroy
On-Card Bytecode Verification for Java Card. E-smart (2001)
Xavier Leroy, François Pessaux
Type-based analysis of uncaught exceptions. ACM Trans. Program. Lang. Syst. 22 (2) (2000)
Xavier Leroy
A modular module system. J. Funct. Program. 10 (3) (2000)
François Pessaux, Xavier Leroy
Type-Based Analysis of Uncaught Exceptions. POPL (1999)
Xavier Leroy, François Rouaix
Security Properties of Typed Applets. Secure Internet Programming (1999)
Xavier Leroy, François Rouaix
Security Properties of Typed Applets. POPL (1998)
Xavier Leroy
Introduction. Types in Compilation (1998)
Xavier Leroy
A Syntactic Theory of Type Generativity and Sharing. J. Funct. Program. 6 (5) (1996)
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
Benchmarking Implementations of Functional Languages with 'Pseudoknot', a Float-Intensive Benchmark. J. Funct. Program. 6 (4) (1996)
Xavier Leroy
Applicative Functors and Fully Transparent Higher-Order Modules. POPL (1995)
Xavier Leroy
Manifest Types, Modules, and Separate Compilation. POPL (1994)
Xavier Leroy, Michel Mauny
Dynamics in ML. J. Funct. Program. 3 (4) (1993)
Damien Doligez, Xavier Leroy
A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML. POPL (1993)
Xavier Leroy
Polymorphism by Name for References and Continuations. POPL (1993)
Xavier Leroy
Unboxed Objects and Polymorphic Typing. POPL (1992)
Xavier Leroy, Michel Mauny
Dynamics in ML. FPCA (1991)
Xavier Leroy, Pierre Weis
Polymorphic Type Inference and Assignment. POPL (1991)
Luca Cardelli, Xavier Leroy
Abstract Types and the Dot Notation. Programming Concepts and Methods (1990)
Xavier Leroy
Efficient Data Representation in Polymorphic Languages. PLILP (1990)

Xavier Leroy.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Xavier Leroy