| 2008 |
|---|
| 42 | EE | Jean-Baptiste Tristan,
Xavier Leroy:
Formal verification of translation validators: a case study on instruction scheduling optimizations.
POPL 2008: 17-27 |
| 2007 |
|---|
| 41 | EE | Zaynah Dargaye,
Xavier Leroy:
Mechanized Verification of CPS Transformations.
LPAR 2007: 211-225 |
| 40 | EE | Xavier Leroy:
Formal verification of an optimizing compiler.
MEMOCODE 2007: 25 |
| 39 | EE | Xavier Leroy:
Formal Verification of an Optimizing Compiler.
RTA 2007: 1 |
| 38 | EE | Andrew W. Appel,
Xavier Leroy:
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract).
Electr. Notes Theor. Comput. Sci. 174(5): 95-108 (2007) |
| 2006 |
|---|
| 37 | EE | 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 |
| 36 | EE | Xavier Leroy:
Coinductive Big-Step Operational Semantics.
ESOP 2006: 54-68 |
| 35 | EE | Sandrine Blazy,
Zaynah Dargaye,
Xavier Leroy:
Formal Verification of a C Compiler Front-End.
FM 2006: 460-475 |
| 34 | EE | Xavier Leroy:
Formal certification of a compiler back-end or: programming a compiler with a proof assistant.
POPL 2006: 42-54 |
| 33 | EE | Nick Benton,
Xavier Leroy:
Preface.
Electr. Notes Theor. Comput. Sci. 148(2): 1-2 (2006) |
| 2005 |
|---|
| 32 | EE | Sandrine Blazy,
Xavier Leroy:
Formal Verification of a Memory Model for C-Like Imperative Languages.
ICFEM 2005: 280-299 |
| 31 | EE | Tom Hirschowitz,
Xavier Leroy:
Mixin modules in a call-by-value setting.
ACM Trans. Program. Lang. Syst. 27(5): 857-881 (2005) |
| 2004 |
|---|
| 30 | | 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 |
| 29 | EE | Tom Hirschowitz,
Xavier Leroy,
J. B. Wells:
Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types.
ESOP 2004: 64-78 |
| 28 | EE | Yves Bertot,
Benjamin Grégoire,
Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.
TYPES 2004: 66-81 |
| 2003 |
|---|
| 27 | EE | Xavier Leroy:
Computer Security from a Programming Language and Static Analysis Perspective.
ESOP 2003: 1-9 |
| 26 | EE | Cristiano Calcagno,
Walid Taha,
Liwen Huang,
Xavier Leroy:
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection.
GPCE 2003: 57-76 |
| 25 | EE | Tom Hirschowitz,
Xavier Leroy,
J. B. Wells:
Compilation of extended recursion in call-by-value functional languages.
PPDP 2003: 160-171 |
| 24 | EE | Xavier Leroy:
Java Bytecode Verification: Algorithms and Formalizations.
J. Autom. Reasoning 30(3-4): 235-269 (2003) |
| 2002 |
|---|
| 23 | EE | Tom Hirschowitz,
Xavier Leroy:
Mixin Modules in a Call-by-Value Setting.
ESOP 2002: 6-20 |
| 22 | EE | Benjamin Grégoire,
Xavier Leroy:
A compiled implementation of strong reduction.
ICFP 2002: 235-246 |
| 21 | | Xavier Leroy:
Bytecode verification on Java smart cards.
Softw., Pract. Exper. 32(4): 319-340 (2002) |
| 2001 |
|---|
| 20 | EE | Xavier Leroy:
Java Bytecode Verification: An Overview.
CAV 2001: 265-285 |
| 19 | EE | Xavier Leroy:
On-Card Bytecode Verification for Java Card.
E-smart 2001: 150-164 |
| 2000 |
|---|
| 18 | EE | Xavier Leroy,
François Pessaux:
Type-based analysis of uncaught exceptions.
ACM Trans. Program. Lang. Syst. 22(2): 340-377 (2000) |
| 17 | | Xavier Leroy:
A modular module system.
J. Funct. Program. 10(3): 269-303 (2000) |
| 1999 |
|---|
| 16 | EE | François Pessaux,
Xavier Leroy:
Type-Based Analysis of Uncaught Exceptions.
POPL 1999: 276-290 |
| 15 | | Xavier Leroy,
François Rouaix:
Security Properties of Typed Applets.
Secure Internet Programming 1999: 147-182 |
| 1998 |
|---|
| 14 | | Xavier Leroy,
Atsushi Ohori:
Types in Compilation, Second International Workshop, TIC '98, Kyoto, Japan, March 25-27, 1998, Proceedings
Springer 1998 |
| 13 | EE | Xavier Leroy,
François Rouaix:
Security Properties of Typed Applets.
POPL 1998: 391-403 |
| 12 | EE | Xavier Leroy:
Introduction.
Types in Compilation 1998: 1-8 |
| 1996 |
|---|
| 11 | | Pieter H. Hartel,
Marc Feeley,
Martin 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) |
| 10 | | Xavier Leroy:
A Syntactic Theory of Type Generativity and Sharing.
J. Funct. Program. 6(5): 667-698 (1996) |
| 1995 |
|---|
| 9 | | Xavier Leroy:
Applicative Functors and Fully Transparent Higher-Order Modules.
POPL 1995: 142-153 |
| 1994 |
|---|
| 8 | | Xavier Leroy:
Manifest Types, Modules, and Separate Compilation.
POPL 1994: 109-122 |
| 1993 |
|---|
| 7 | | Damien Doligez,
Xavier Leroy:
A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML.
POPL 1993: 113-123 |
| 6 | | Xavier Leroy:
Polymorphism by Name for References and Continuations.
POPL 1993: 220-231 |
| 5 | | Xavier Leroy,
Michel Mauny:
Dynamics in ML.
J. Funct. Program. 3(4): 431-463 (1993) |
| 1992 |
|---|
| 4 | | Xavier Leroy:
Unboxed Objects and Polymorphic Typing.
POPL 1992: 177-188 |
| 1991 |
|---|
| 3 | | Xavier Leroy,
Michel Mauny:
Dynamics in ML.
FPCA 1991: 406-426 |
| 2 | | Xavier Leroy,
Pierre Weis:
Polymorphic Type Inference and Assignment.
POPL 1991: 291-302 |
| 1990 |
|---|
| 1 | | Xavier Leroy:
Efficient Data Representation in Polymorphic Languages.
PLILP 1990: 255-276 |
