default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDXavier Leroy
Person information
- affiliation: INRIA, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
[j24]Andrew W. Appel
, Xavier Leroy:
Efficient Extensional Binary Tries. J. Autom. Reason. 67(1): 8 (2023)- 2021
- [j23]Nathanaël Courant, Xavier Leroy:
Verified code generation for the polyhedral model. Proc. ACM Program. Lang. 5(POPL): 1-24 (2021) - [i6]Andrew W. Appel, Xavier Leroy:
Efficient Extensional Binary Tries. CoRR abs/2110.05063 (2021)
2010 – 2019
- 2018
- [c53]Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, Simon Wegener:
Embedded Program Annotations for WCET Analysis. WCET 2018: 8:1-8:13 - 2017
- [c52]Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg:
A formally verified compiler for Lustre. PLDI 2017: 586-601 - 2016
- [c51]Xavier Leroy:
Formally Verifying a Compiler: What Does It Mean, Exactly? ICALP 2016: 2:1-2:1 - 2015
- [j22]Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond:
Verified Compilation of Floating-Point Computations. J. Autom. Reason. 54(2): 135-163 (2015) - [c50]Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie:
A Formally-Verified C Static Analyzer. POPL 2015: 247-259 - [e4]Xavier Leroy, Alwen Tiu:
Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015. ACM 2015, ISBN 978-1-4503-3296-5 [contents] - 2014
- [c49]Xavier Leroy:
Compiler verification for fun and profit. FMCAD 2014: 9 - [c48]Robbert Krebbers, Xavier Leroy, Freek Wiedijk:
Formal C Semantics: CompCert and the C Standard. ITP 2014: 543-548 - [c47]Xavier Leroy:
Formal Proofs of Code Generation and Verification Tools. SEFM 2014: 1-4 - 2013
- [c46]Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond:
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic 2013: 107-115 - 2012
- [j21]Andrew W. Appel, Robert Dockins, Xavier Leroy:
A List-Machine Benchmark for Mechanized Metatheory. J. Autom. Reason. 49(3): 453-491 (2012) - [c45]Xavier Leroy:
Mechanized Semantics for Compiler Verification. APLAS 2012: 386-388 - [c44]Xavier Leroy:
Mechanized Semantics for Compiler Verification. CPP 2012: 4-6 - [c43]Valentin Robert, Xavier Leroy:
A Formally-Verified Alias Analysis. CPP 2012: 11-26 - [c42]Jacques-Henri Jourdan, François Pottier, Xavier Leroy:
Validating LR(1) Parsers. ESOP 2012: 397-416 - [c41]Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy:
A mechanized semantics for C++ object construction and destruction, with applications to resource management. POPL 2012: 521-532 - 2011
- [j20]Xavier Leroy:
Safety first!: technical perspective. Commun. ACM 54(12): 122 (2011) - [j19]Andrew P. Tolmach, Xavier Leroy:
Special Issue Dedicated to ICFP 2009 Editorial. J. Funct. Program. 21(4-5): 331-332 (2011) - [c40]Xavier Leroy:
Formally verifying a compiler: Why? How? How far? CGO 2011 - [c39]Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris:
Towards Formally Verified Optimizing Compilation in Flight Control Software. PPES 2011: 59-68 - [c38]Xavier Leroy:
Verified squared: does critical software deserve verified tools? POPL 2011: 1-2 - [c37]Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy:
Formal verification of object layout for c++ multiple inheritance. POPL 2011: 67-80 - 2010
- [c36]Silvain Rideau, Xavier Leroy:
Validating Register Allocation and Spilling. CC 2010: 224-243 - [c35]Jean-Baptiste Tristan, Xavier Leroy:
A simple, verified validator for software pipelining. POPL 2010: 83-92 - [p1]Xavier Leroy:
Mechanized semantics - with applications to program proof and compiler verification. Logics and Languages for Reliability and Security 2010: 195-224 - [i5]Xavier Leroy:
Mechanized semantics. CoRR abs/1010.5582 (2010)
2000 – 2009
- 2009
- [j18]Xavier Leroy:
Formal verification of a realistic compiler. Commun. ACM 52(7): 107-115 (2009) - [j17]Xavier Leroy, Hervé Grall:
Coinductive big-step operational semantics. Inf. Comput. 207(2): 284-304 (2009) - [j16]Sandrine Blazy, Xavier Leroy:
Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reason. 43(3): 263-288 (2009) - [j15]Xavier Leroy:
A Formally Verified Compiler Back-end. J. Autom. Reason. 43(4): 363-446 (2009) - [j14]Xavier Leroy:
Editorial. J. Funct. Program. 19(2): 143 (2009) - [j13]Xavier Leroy, Matthias Felleisen:
Editorial. J. Funct. Program. 19(5): 489-490 (2009) - [j12]Tom Hirschowitz, Xavier Leroy, J. B. Wells:
Compilation of extended recursion in call-by-value functional languages. High. Order Symb. Comput. 22(1): 3-66 (2009) - [j11]Zaynah Dargaye, Xavier Leroy:
A verified framework for higher-order uncurrying optimizations. High. Order Symb. Comput. 22(3): 199-231 (2009) - [c34]Jean-Baptiste Tristan, Xavier Leroy:
Verified validation of lazy code motion. PLDI 2009: 316-326 - [i4]Sandrine Blazy, Xavier Leroy:
Mechanized semantics for the Clight subset of the C language. CoRR abs/0901.3619 (2009) - [i3]Tom Hirschowitz, Xavier Leroy, J. B. Wells:
Compilation of extended recursion in call-by-value functional languages. CoRR abs/0902.1257 (2009) - [i2]Xavier Leroy:
A formally verified compiler back-end. CoRR abs/0902.2137 (2009) - 2008
- [j10]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): 307-326 (2008) - [j9]Xavier Leroy, Sandrine Blazy:
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reason. 41(1): 1-31 (2008) - [c33]Jean-Baptiste Tristan, Xavier Leroy:
Formal verification of translation validators: a case study on instruction scheduling optimizations. POPL 2008: 17-27 - [i1]Xavier Leroy, Hervé Grall:
Coinductive big-step operational semantics. CoRR abs/0808.0586 (2008) - 2007
- [c32]Zaynah Dargaye, Xavier Leroy:
Mechanized Verification of CPS Transformations. LPAR 2007: 211-225 - [c31]Xavier Leroy:
Formal verification of an optimizing compiler. MEMOCODE 2007: 25 - [c30]Xavier Leroy:
Formal Verification of an Optimizing Compiler. RTA 2007: 1 - 2006
- [c29]Xavier Leroy:
Coinductive Big-Step Operational Semantics. ESOP 2006: 54-68 - [c28]Sandrine Blazy, Zaynah Dargaye, Xavier Leroy:
Formal Verification of a C Compiler Front-End. FM 2006: 460-475 - [c27]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: 199-208 - [c26]Xavier Leroy:
Formal certification of a compiler back-end or: programming a compiler with a proof assistant. POPL 2006: 42-54 - [c25]Andrew W. Appel, Xavier Leroy:
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). LFMTP@FLoC 2006: 95-108 - [e3]Nick Benton, Xavier Leroy:
Proceedings of the ACM-SIGPLAN Workshop on ML, ML 2005, Tallinn, Estonia, September 29, 2005. Electronic Notes in Theoretical Computer Science 148(2), Elsevier 2006 [contents] - 2005
- [j8]Tom Hirschowitz, Xavier Leroy:
Mixin modules in a call-by-value setting. ACM Trans. Program. Lang. Syst. 27(5): 857-881 (2005) - [c24]Sandrine Blazy, Xavier Leroy:
Formal Verification of a Memory Model for C-Like Imperative Languages. ICFEM 2005: 280-299 - [c23]Nick Benton, Xavier Leroy:
Preface. ML 2005: 1-2 - 2004
- [c22]Tom Hirschowitz, Xavier Leroy, J. B. Wells:
Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types. ESOP 2004: 64-78 - [c21]Yves Bertot, Benjamin Grégoire, Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81 - [e2]Neil D. Jones, Xavier Leroy:
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004. ACM 2004, ISBN 1-58113-729-X [contents] - 2003
- [j7]Xavier Leroy:
Java Bytecode Verification: Algorithms and Formalizations. J. Autom. Reason. 30(3-4): 235-269 (2003) - [c20]Xavier Leroy:
Computer Security from a Programming Language and Static Analysis Perspective. ESOP 2003: 1-9 - [c19]Cristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy:
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. GPCE 2003: 57-76 - [c18]Tom Hirschowitz, Xavier Leroy, J. B. Wells:
Compilation of extended recursion in call-by-value functional languages. PPDP 2003: 160-171 - 2002
- [j6]Xavier Leroy:
Bytecode verification on Java smart cards. Softw. Pract. Exp. 32(4): 319-340 (2002) - [c17]Tom Hirschowitz, Xavier Leroy:
Mixin Modules in a Call-by-Value Setting. ESOP 2002: 6-20 - [c16]Benjamin Grégoire, Xavier Leroy:
A compiled implementation of strong reduction. ICFP 2002: 235-246 - 2001
- [c15]Xavier Leroy:
Java Bytecode Verification: An Overview. CAV 2001: 265-285 - [c14]Xavier Leroy:
On-Card Bytecode Verification for Java Card. E-smart 2001: 150-164 - 2000
- [j5]Xavier Leroy:
A modular module system. J. Funct. Program. 10(3): 269-303 (2000) - [j4]Xavier Leroy, François Pessaux:
Type-based analysis of uncaught exceptions. ACM Trans. Program. Lang. Syst. 22(2): 340-377 (2000)
1990 – 1999
- 1999
- [c13]Xavier Leroy, François Rouaix:
Security Properties of Typed Applets. Secure Internet Programming 1999: 147-182 - [c12]François Pessaux, Xavier Leroy:
Type-Based Analysis of Uncaught Exceptions. POPL 1999: 276-290 - 1998
- [c11]Xavier Leroy, François Rouaix:
Security Properties of Typed Applets. POPL 1998: 391-403 - [c10]Xavier Leroy:
Introduction. Types in Compilation 1998: 1-8 - [e1]Xavier Leroy, Atsushi Ohori:
Types in Compilation, Second International Workshop, TIC '98, Kyoto, Japan, March 25-27, 1998, Proceedings. Lecture Notes in Computer Science 1473, Springer 1998, ISBN 3-540-64925-5 [contents] - 1996
- [j3]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): 621-655 (1996) - [j2]Xavier Leroy:
A Syntactic Theory of Type Generativity and Sharing. J. Funct. Program. 6(5): 667-698 (1996) - 1995
- [c9]Xavier Leroy:
Applicative Functors and Fully Transparent Higher-Order Modules. POPL 1995: 142-153 - 1994
- [c8]Xavier Leroy:
Manifest Types, Modules, and Separate Compilation. POPL 1994: 109-122 - 1993
- [b3]Xavier Leroy, Pierre Weis:
Manuel de référence du langage CAML. InterEditions 1993, ISBN 978-2-7296-0492-9, pp. I-X, 1-166 - [b2]Pierre Weis, Xavier Leroy:
Le langage Caml. InterEditions 1993, ISBN 978-2-7296-0493-6, pp. I-XIII, 1-407 - [j1]Xavier Leroy, Michel Mauny:
Dynamics in ML. J. Funct. Program. 3(4): 431-463 (1993) - [c7]Damien Doligez, Xavier Leroy:
A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML. POPL 1993: 113-123 - [c6]Xavier Leroy:
Polymorphism by Name for References and Continuations. POPL 1993: 220-231 - 1992
- [b1]Xavier Leroy:
Typage polymorphe d'un langage algorithmique. (Polymorphic typing of an algorithmic language). Paris Diderot University, France, 1992 - [c5]Xavier Leroy:
Unboxed Objects and Polymorphic Typing. POPL 1992: 177-188 - 1991
- [c4]Xavier Leroy, Michel Mauny:
Dynamics in ML. FPCA 1991: 406-426 - [c3]Xavier Leroy, Pierre Weis:
Polymorphic Type Inference and Assignment. POPL 1991: 291-302 - 1990
- [c2]Luca Cardelli, Xavier Leroy:
Abstract Types and the Dot Notation. Programming Concepts and Methods 1990: 479-504 - [c1]Xavier Leroy:
Efficient Data Representation in Polymorphic Languages. PLILP 1990: 255-276
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 23:20 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
