Xavier Leroy - RankMe

93 papers A* 21A 7B 11C 4Journal 32Unranked 12

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