Abstract Types and the Dot Notation. - Luca Cardelli; Xavier Leroy (Programming Concepts and Methods, 1990)

Efficient Data Representation in Polymorphic Languages. - Xavier Leroy (PLILP, 1990)

Polymorphic Type Inference and Assignment. - Xavier Leroy; Pierre Weis (POPL, 1991)

Unboxed Objects and Polymorphic Typing. - Xavier Leroy (POPL, 1992)

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

Le langage Caml. - Pierre Weis; Xavier Leroy (InterEditions, 1993)

Manuel de référence du langage CAML. - Xavier Leroy; Pierre Weis (InterEditions, 1993)

A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML. - Damien Doligez; Xavier Leroy (POPL, 1993)

Polymorphism by Name for References and Continuations. - Xavier Leroy (POPL, 1993)

Dynamics in ML. - Xavier Leroy; Michel Mauny (J. Funct. Program., 1993)

Manifest Types, Modules, and Separate Compilation. - Xavier Leroy (POPL, 1994)

Applicative Functors and Fully Transparent Higher-Order Modules. - Xavier Leroy (POPL, 1995)

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; et al. (J. Funct. Program., 1996)

A Syntactic Theory of Type Generativity and Sharing. - Xavier Leroy (J. Funct. Program., 1996)

Introduction. - Xavier Leroy (Types in Compilation, 1998)

Security Properties of Typed Applets. - Xavier Leroy; François Rouaix (Secure Internet Programming, 1999)

A modular module system. - Xavier Leroy (J. Funct. Program., 2000)

Type-based analysis of uncaught exceptions. - Xavier Leroy; François Pessaux (ACM Trans. Program. Lang. Syst., 2000)

Java Bytecode Verification: An Overview. - Xavier Leroy (CAV, 2001)

On-Card Bytecode Verification for Java Card. - Xavier Leroy (E-smart, 2001)

A compiled implementation of strong reduction. - Benjamin Grégoire; Xavier Leroy (ICFP, 2002)

Bytecode verification on Java smart cards. - Xavier Leroy (Softw. Pract. Exp., 2002)

Computer Security from a Programming Language and Static Analysis Perspective. - Xavier Leroy (ESOP, 2003)

Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. - Cristiano Calcagno; Walid Taha; Liwen Huang; Xavier Leroy (GPCE, 2003)

Java Bytecode Verification: Algorithms and Formalizations. - Xavier Leroy (J. Autom. Reason., 2003)

Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types. - Tom Hirschowitz; Xavier Leroy; J. B. Wells (ESOP, 2004)

A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. - Yves Bertot; Benjamin Grégoire; Xavier Leroy (TYPES, 2004)

Formal Verification of a Memory Model for C-Like Imperative Languages. - Sandrine Blazy; Xavier Leroy (ICFEM, 2005)

Preface. - Nick Benton; Xavier Leroy (ML, 2005)

Mixin modules in a call-by-value setting. - Tom Hirschowitz; Xavier Leroy (ACM Trans. Program. Lang. Syst., 2005)

Coinductive Big-Step Operational Semantics. - Xavier Leroy (ESOP, 2006)

Formal Verification of a C Compiler Front-End. - Sandrine Blazy; Zaynah Dargaye; Xavier Leroy (FM, 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 (ASE, 2006)

Formal certification of a compiler back-end or: programming a compiler with a proof assistant. - Xavier Leroy (POPL, 2006)

A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). - Andrew W. Appel; Xavier Leroy (LFMTP@FLoC, 2006)

Mechanized Verification of CPS Transformations. - Zaynah Dargaye; Xavier Leroy (LPAR, 2007)

Formal verification of an optimizing compiler. - Xavier Leroy (MEMOCODE, 2007)

Formal verification of translation validators: a case study on instruction scheduling optimizations. - Jean-Baptiste Tristan; Xavier Leroy (POPL, 2008)

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. - Xavier Leroy; Sandrine Blazy (J. Autom. Reason., 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)

Verified validation of lazy code motion. - Jean-Baptiste Tristan; Xavier Leroy (PLDI, 2009)

Formal verification of a realistic compiler. - Xavier Leroy (Commun. ACM, 2009)

Coinductive big-step operational semantics. - Xavier Leroy; Hervé Grall (Inf. Comput., 2009)

Mechanized Semantics for the Clight Subset of the C Language. - Sandrine Blazy; Xavier Leroy (J. Autom. Reason., 2009)

A Formally Verified Compiler Back-end. - Xavier Leroy (J. Autom. Reason., 2009)

Editorial. - Xavier Leroy (J. Funct. Program., 2009)

Editorial. - Xavier Leroy; Matthias Felleisen (J. Funct. Program., 2009)

A verified framework for higher-order uncurrying optimizations. - Zaynah Dargaye; Xavier Leroy (High. Order Symb. Comput., 2009)

Compilation of extended recursion in call-by-value functional languages. - Tom Hirschowitz; Xavier Leroy; J. B. Wells (High. Order Symb. Comput., 2009)

Validating Register Allocation and Spilling. - Silvain Rideau; Xavier Leroy (CC, 2010)

A simple, verified validator for software pipelining. - Jean-Baptiste Tristan; Xavier Leroy (POPL, 2010)

Mechanized semantics - Xavier Leroy (CoRR, 2010)

Mechanized semantics - with applications to program proof and compiler verification. - Xavier Leroy (Logics and Languages for Reliability and Security, 2010)

Formally verifying a compiler: Why? How? How far? - Xavier Leroy (CGO, 2011)

Towards Formally Verified Optimizing Compilation in Flight Control Software. - Ricardo Bedin França; Denis Favre-Felix; Xavier Leroy; Marc Pantel; Jean Souyris (PPES, 2011)

Verified squared: does critical software deserve verified tools? - Xavier Leroy (POPL, 2011)

Formal verification of object layout for c++ multiple inheritance. - Tahina Ramananandro; Gabriel Dos Reis; Xavier Leroy (POPL, 2011)

Safety first!: technical perspective. - Xavier Leroy (Commun. ACM, 2011)

Special Issue Dedicated to ICFP 2009 Editorial. - Andrew P. Tolmach; Xavier Leroy (J. Funct. Program., 2011)

Mechanized Semantics for Compiler Verification. - Xavier Leroy (APLAS, 2012)

A Formally-Verified Alias Analysis. - Valentin Robert; Xavier Leroy (CPP, 2012)

Validating LR(1) Parsers. - Jacques-Henri Jourdan; François Pottier; Xavier Leroy (ESOP, 2012)

A mechanized semantics for C++ object construction and destruction, with applications to resource management. - Tahina Ramananandro; Gabriel Dos Reis; Xavier Leroy (POPL, 2012)

A List-Machine Benchmark for Mechanized Metatheory. - Andrew W. Appel; Robert Dockins; Xavier Leroy (J. Autom. Reason., 2012)

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. - Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond (IEEE Symposium on Computer Arithmetic, 2013)

Compiler verification for fun and profit. - Xavier Leroy (FMCAD, 2014)

Formal C Semantics: CompCert and the C Standard. - Robbert Krebbers; Xavier Leroy; Freek Wiedijk (ITP, 2014)

Formal Proofs of Code Generation and Verification Tools. - Xavier Leroy (SEFM, 2014)

A Formally-Verified C Static Analyzer. - Jacques-Henri Jourdan; Vincent Laporte; Sandrine Blazy; Xavier Leroy; David Pichardie (POPL, 2015)

Verified Compilation of Floating-Point Computations. - Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond (J. Autom. Reason., 2015)

Formally Verifying a Compiler: What Does It Mean, Exactly? - Xavier Leroy (ICALP, 2016)

A formally verified compiler for Lustre. - Timothy Bourke; Lélio Brun; Pierre-Évariste Dagand; Xavier Leroy; Marc Pouzet; Lionel Rieg (PLDI, 2017)

Embedded Program Annotations for WCET Analysis. - Bernhard Schommer; Christoph Cullmann; Gernot Gebhard; Xavier Leroy; Michael Schmidt 007; Simon Wegener (WCET, 2018)

Verified code generation for the polyhedral model. - Nathanaël Courant; Xavier Leroy (Proc. ACM Program. Lang., 2021)

Efficient Extensional Binary Tries. - Andrew W. Appel; Xavier Leroy (J. Autom. Reason., 2023)