dblp.uni-trier.dewww.uni-trier.de

Xavier Leroy Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo

*2009
52EEJean-Baptiste Tristan, Xavier Leroy: Verified validation of lazy code motion. PLDI 2009: 316-326
51EESandrine Blazy, Xavier Leroy: Mechanized semantics for the Clight subset of the C language CoRR abs/0901.3619: (2009)
50EETom Hirschowitz, Xavier Leroy, J. B. Wells: Compilation of extended recursion in call-by-value functional languages CoRR abs/0902.1257: (2009)
49EEXavier Leroy: A formally verified compiler back-end CoRR abs/0902.2137: (2009)
48EEXavier Leroy: Formal verification of a realistic compiler. Commun. ACM 52(7): 107-115 (2009)
47EEXavier Leroy, Hervé Grall: Coinductive big-step operational semantics. Inf. Comput. 207(2): 284-304 (2009)
46EEXavier Leroy: Editorial. J. Funct. Program. 19(2): 143 (2009)
2008
45EEJean-Baptiste Tristan, Xavier Leroy: Formal verification of translation validators: a case study on instruction scheduling optimizations. POPL 2008: 17-27
44EEXavier Leroy, Hervé Grall: Coinductive big-step operational semantics CoRR abs/0808.0586: (2008)
43EELaurence Rideau, Bernard P. Serpette, Xavier Leroy: Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves. J. Autom. Reasoning 40(4): 307-326 (2008)
42EEXavier Leroy, Sandrine Blazy: Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reasoning 41(1): 1-31 (2008)
2007
41EEZaynah Dargaye, Xavier Leroy: Mechanized Verification of CPS Transformations. LPAR 2007: 211-225
40EEXavier Leroy: Formal verification of an optimizing compiler. MEMOCODE 2007: 25
39EEXavier Leroy: Formal Verification of an Optimizing Compiler. RTA 2007: 1
38EEAndrew W. Appel, Xavier Leroy: A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). Electr. Notes Theor. Comput. Sci. 174(5): 95-108 (2007)
2006
37EEFabio 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
36EEXavier Leroy: Coinductive Big-Step Operational Semantics. ESOP 2006: 54-68
35EESandrine Blazy, Zaynah Dargaye, Xavier Leroy: Formal Verification of a C Compiler Front-End. FM 2006: 460-475
34EEXavier Leroy: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. POPL 2006: 42-54
33EENick Benton, Xavier Leroy: Preface. Electr. Notes Theor. Comput. Sci. 148(2): 1-2 (2006)
2005
32EESandrine Blazy, Xavier Leroy: Formal Verification of a Memory Model for C-Like Imperative Languages. ICFEM 2005: 280-299
31EETom 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
29EETom Hirschowitz, Xavier Leroy, J. B. Wells: Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types. ESOP 2004: 64-78
28EEYves Bertot, Benjamin Grégoire, Xavier Leroy: A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81
2003
27EEXavier Leroy: Computer Security from a Programming Language and Static Analysis Perspective. ESOP 2003: 1-9
26EECristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy: Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. GPCE 2003: 57-76
25EETom Hirschowitz, Xavier Leroy, J. B. Wells: Compilation of extended recursion in call-by-value functional languages. PPDP 2003: 160-171
24EEXavier Leroy: Java Bytecode Verification: Algorithms and Formalizations. J. Autom. Reasoning 30(3-4): 235-269 (2003)
2002
23EETom Hirschowitz, Xavier Leroy: Mixin Modules in a Call-by-Value Setting. ESOP 2002: 6-20
22EEBenjamin 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
20EEXavier Leroy: Java Bytecode Verification: An Overview. CAV 2001: 265-285
19EEXavier Leroy: On-Card Bytecode Verification for Java Card. E-smart 2001: 150-164
2000
18EEXavier 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
16EEFranç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
13EEXavier Leroy, François Rouaix: Security Properties of Typed Applets. POPL 1998: 391-403
12EEXavier 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
1EEXavier Leroy: Efficient Data Representation in Polymorphic Languages. PLILP 1990: 255-276

Coauthor Index

1Martin Alt [11]
2Andrew W. Appel [38]
3Lennart Augustsson [11]
4Peter Baumann [11]
5Marcel Beemster [11]
6Nick Benton (P. N. Benton) [33]
7Yves Bertot [28]
8Sandrine Blazy [32] [35] [42] [51]
9Jaap Boender [37]
10Cristiano Calcagno [26]
11Emmanuel Chailloux [11]
12Roberto Di Cosmo [37]
13Zaynah Dargaye [35] [41]
14Damien Doligez [7]
15Berke Durak [37]
16Marc Feeley [11]
17Christine H. Flood [11]
18Hervé Grall [44] [47]
19Benjamin Grégoire [22] [28]
20Wolfgang Grieskamp [11]
21John H. G. van Groningen [11]
22Kevin Hammond [11]
23Pieter H. Hartel [11]
24Bogumil Hausman [11]
25Tom Hirschowitz [23] [25] [29] [31] [50]
26Liwen Huang [26]
27Melody Y. Ivory [11]
28Neil D. Jones [30]
29Richard E. Jones [11]
30Jasper Kamperman [11]
31Peter Lee [11]
32Rafael Dueire Lins [11]
33Sandra Loosemore [11]
34Fabio Mancinelli [37]
35Michel Mauny [3] [5]
36Atsushi Ohori [14]
37François Pessaux [16] [18]
38Laurence Rideau [43]
39Niklas Röjemo [11]
40François Rouaix [13] [15]
41Bernard P. Serpette [43]
42Manuel Serrano [11]
43Walid Taha [26]
44Jean-Pierre Talpin [11]
45Jon Thackray [11]
46Stephen Thomas [11]
47Ralf Treinen [37]
48Jean-Baptiste Tristan [45] [52]
49Jérôme Vouillon (Jerome Vouillon) [37]
50Pum Walters [11]
51Pierre Weis [2] [11]
52J. B. Wells [25] [29] [50]
53Peter Wentworth [11]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)