Xavier Leroy - researchr profile publications

researchr

You are not signed in
Sign in
Sign up

2010

Validating Register Allocation and SpillingSilvain Rideau, Xavier Leroy. CC 2010: 224-243 [doi]

A simple, verified validator for software pipeliningJean-Baptiste Tristan, Xavier Leroy. POPL 2010: 83-92 [doi]

2009

Mechanized Semantics for the Clight Subset of the C LanguageSandrine Blazy, Xavier Leroy. JAR, 43(3):263-288, 2009. [doi]

A verified framework for higher-order uncurrying optimizationsZaynah Dargaye, Xavier Leroy. lisp, 22(3):199-231, 2009. [doi]

Compilation of extended recursion in call-by-value functional languagesTom Hirschowitz, Xavier Leroy, J. B. Wells. lisp, 22(1):3-66, 2009. [doi]

EditorialXavier Leroy. JFP, 19(2):143, 2009. [doi]

EditorialXavier Leroy, Matthias Felleisen. JFP, 19(5):489-490, 2009. [doi]

Coinductive big-step operational semanticsXavier Leroy, Hervé Grall. iandc, 207(2):284-304, 2009. [doi]

A Formally Verified Compiler Back-endXavier Leroy. JAR, 43(4):363-446, 2009. [doi]

Formal verification of a realistic compilerXavier Leroy. CACM, 52(7):107-115, 2009. [doi]

Verified validation of lazy code motionJean-Baptiste Tristan, Xavier Leroy. PLDI 2009: 316-326 [doi]

2008

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program TransformationsXavier Leroy, Sandrine Blazy. JAR, 41(1):1-31, 2008. [doi]

Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel MovesLaurence Rideau, Bernard P. Serpette, Xavier Leroy. JAR, 40(4):307-326, 2008. [doi]

Formal verification of translation validators: a case study on instruction scheduling optimizationsJean-Baptiste Tristan, Xavier Leroy. POPL 2008: 17-27 [doi]

2007

A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract)Andrew W. Appel, Xavier Leroy. ENTCS, 174(5):95-108, 2007. [doi]

Mechanized Verification of CPS TransformationsZaynah Dargaye, Xavier Leroy. lpar 2007: 211-225 [doi]

Formal verification of an optimizing compilerXavier Leroy. memocode 2007: 25 [doi]

Formal Verification of an Optimizing CompilerXavier Leroy. RTA 2007: 1 [doi]

2006

2005

Formal Verification of a Memory Model for ::::C::::-Like Imperative LanguagesSandrine Blazy, Xavier Leroy. icfem 2005: 280-299 [doi]

Mixin modules in a call-by-value settingTom Hirschowitz, Xavier Leroy. TOPLAS, 27(5):857-881, 2005. [doi]

2004

A Structured Approach to Proving Compiler Optimizations Based on Dataflow AnalysisYves Bertot, Benjamin Grégoire, Xavier Leroy. TYPES 2006: 66-81 [doi]

Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, TypesTom Hirschowitz, Xavier Leroy, J. B. Wells. ESOP 2004: 64-78 [doi]

Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004Neil D. Jones, Xavier Leroy, editors, ACM, 2004.

2003

Implementing multi-stage languages using ASTs, Gensym, and reflectionCalcagno, Cristiano, Walid Taha, Huang, Liwen, Xavier Leroy. In GPCE '03: Proceedings of the 2nd international conference on Generative programming and component engineering. 2003:

Implementing Multi-stage Languages Using ASTs, Gensym, and ReflectionCristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy. GPCE 2003: 57-76 [doi]

Compilation of extended recursion in call-by-value functional languagesTom Hirschowitz, Xavier Leroy, J. B. Wells. ppdp 2003: 160-171 [doi]

Java Bytecode Verification: Algorithms and FormalizationsXavier Leroy. JAR, 30(3-4):235-269, 2003. [doi]

Computer Security from a Programming Language and Static Analysis PerspectiveXavier Leroy. ESOP 2003: 1-9 [doi]

2002

A compiled implementation of strong reductionBenjamin Grégoire, Xavier Leroy. ICFP 2002: 235-246 [doi]

Mixin Modules in a Call-by-Value SettingTom Hirschowitz, Xavier Leroy. ESOP 2002: 6-20 [doi]

Bytecode verification on Java smart cardsXavier Leroy. SPE, 32(4):319-340, 2002.

2001

On-Card Bytecode Verification for Java CardXavier Leroy. esmart 2001: 150-164 [doi]

Java Bytecode Verification: An OverviewXavier Leroy. cav 2001: 265-285 [doi]

2000

A modular module systemXavier Leroy. JFP, 10(3):269-303, 2000.

Type-based analysis of uncaught exceptionsXavier Leroy, François Pessaux. TOPLAS, 22(2):340-377, 2000. [doi]

1999

Security Properties of Typed AppletsXavier Leroy, François Rouaix. ECOOPW 1999: 147-182

Type-Based Analysis of Uncaught ExceptionsFrançois Pessaux, Xavier Leroy. POPL 1999: 276-290 [doi]

1998

Types in Compilation, Second International Workshop, TIC 98, Kyoto, Japan, March 25-27, 1998, ProceedingsXavier Leroy, Atsushi Ohori, editors, Volume 1473 of Lecture Notes in Computer Science, Springer, 1998.

IntroductionXavier Leroy. tic 1998: 1-8 [doi]

Security Properties of Typed AppletsXavier Leroy, François Rouaix. POPL 1998: 391-403 [doi]

1996

1995

Applicative Functors and Fully Transparent Higher-Order ModulesXavier Leroy. POPL 1995: 142-153

1994

Manifest Types, Modules, and Separate CompilationXavier Leroy. POPL 1994: 109-122

1993

A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of MLDamien Doligez, Xavier Leroy. POPL 1993: 113-123

Dynamics in MLXavier Leroy, Michel Mauny. JFP, 3(4):431-463, 1993.

Polymorphism by Name for References and ContinuationsXavier Leroy. POPL 1993: 220-231

1992

Unboxed Objects and Polymorphic TypingXavier Leroy. POPL 1992: 177-188

1991

Dynamics in MLXavier Leroy, Michel Mauny. fpca 1991: 406-426

Polymorphic Type Inference and AssignmentXavier Leroy, Pierre Weis. POPL 1991: 291-302

1990

Efficient Data Representation in Polymorphic LanguagesXavier Leroy. plilp 1990: 255-276