| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy |
A mechanized semantics for C++ object construction and destruction, with applications to resource management.  |
POPL  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques-Henri Jourdan, François Pottier, Xavier Leroy |
Validating LR(1) Parsers. |
ESOP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Safety first!: technical perspective. |
Commun. ACM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew P. Tolmach, Xavier Leroy |
Special Issue Dedicated to ICFP 2009 Editorial. |
J. Funct. Program. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Formally verifying a compiler: Why? How? How far? |
CGO |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Verified squared: does critical software deserve verified tools? |
POPL |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy |
Formal verification of object layout for c++ multiple inheritance. |
POPL |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris |
Towards Formally Verified Optimizing Compilation in Flight Control Software. |
PPES |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Mechanized semantics |
CoRR |
2010 |
DBLP BibTeX RDF |
|
| 1 | Xavier Leroy |
Mechanized semantics - with applications to program proof and compiler verification. |
Logics and Languages for Reliability and Security |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Baptiste Tristan, Xavier Leroy |
A simple, verified validator for software pipelining. |
POPL |
2010 |
DBLP DOI BibTeX RDF |
software pipelining, translation validation, verified compilers, symbolic evaluation |
| 1 | Silvain Rideau, Xavier Leroy |
Validating Register Allocation and Spilling. |
CC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy, Hervé Grall |
Coinductive big-step operational semantics. |
Inf. Comput. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Formal verification of a realistic compiler. |
Commun. ACM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
A formally verified compiler back-end |
CoRR |
2009 |
DBLP BibTeX RDF |
|
| 1 | Tom Hirschowitz, Xavier Leroy, J. B. Wells |
Compilation of extended recursion in call-by-value functional languages |
CoRR |
2009 |
DBLP BibTeX RDF |
|
| 1 | Sandrine Blazy, Xavier Leroy |
Mechanized semantics for the Clight subset of the C language |
CoRR |
2009 |
DBLP BibTeX RDF |
|
| 1 | Xavier Leroy |
A Formally Verified Compiler Back-end. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandrine Blazy, Xavier Leroy |
Mechanized Semantics for the Clight Subset of the C Language. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Zaynah Dargaye, Xavier Leroy |
A verified framework for higher-order uncurrying optimizations. |
Higher-Order and Symbolic Computation |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Tom Hirschowitz, Xavier Leroy, J. B. Wells |
Compilation of extended recursion in call-by-value functional languages. |
Higher-Order and Symbolic Computation |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Editorial. |
J. Funct. Program. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy, Matthias Felleisen |
Editorial. |
J. Funct. Program. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Baptiste Tristan, Xavier Leroy |
Verified validation of lazy code motion. |
PLDI |
2009 |
DBLP DOI BibTeX RDF |
lazy code motion, the coq proof assistant, redundancy elimination, translation validation, verified compilers |
| 1 | Xavier Leroy, Hervé Grall |
Coinductive big-step operational semantics |
CoRR |
2008 |
DBLP BibTeX RDF |
|
| 1 | Laurence Rideau, Bernard P. Serpette, Xavier Leroy |
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves. |
J. Autom. Reasoning |
2008 |
DBLP DOI BibTeX RDF |
Parallel move, Parallel assignment, The Coq proof assistant, Compilation, Compiler correctness |
| 1 | Xavier Leroy, Sandrine Blazy |
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. |
J. Autom. Reasoning |
2008 |
DBLP DOI BibTeX RDF |
The Coq proof assistant, Compilation, C, Program verification, Memory model, Compiler correctness |
| 1 | Jean-Baptiste Tristan, Xavier Leroy |
Formal verification of translation validators: a case study on instruction scheduling optimizations. |
POPL |
2008 |
DBLP DOI BibTeX RDF |
the coq proof assistant, translation validation, scheduling optimizations, verified compilers |
| 1 | Andrew W. Appel, Xavier Leroy |
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Formal verification of an optimizing compiler. |
MEMOCODE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Zaynah Dargaye, Xavier Leroy |
Mechanized Verification of CPS Transformations. |
LPAR |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Formal Verification of an Optimizing Compiler. |
RTA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Nick Benton, Xavier Leroy |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Formal certification of a compiler back-end or: programming a compiler with a proof assistant. |
POPL |
2006 |
DBLP DOI BibTeX RDF |
compiler transformations and optimizations, the Coq theorem prover, certified compilation, program proof, semantic preservation |
| 1 | Sandrine Blazy, Zaynah Dargaye, Xavier Leroy |
Formal Verification of a C Compiler Front-End. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Coinductive Big-Step Operational Semantics. |
ESOP |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Tom Hirschowitz, Xavier Leroy |
Mixin modules in a call-by-value setting. |
ACM Trans. Program. Lang. Syst. |
2005 |
DBLP DOI BibTeX RDF |
type systems, recursion, modules, Mixins |
| 1 | Sandrine Blazy, Xavier Leroy |
Formal Verification of a Memory Model for C-Like Imperative Languages. |
ICFEM |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Neil D. Jones, Xavier Leroy (eds.) |
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004 |
POPL |
2004 |
DBLP BibTeX RDF |
|
| 1 | Yves Bertot, Benjamin Grégoire, Xavier Leroy |
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Tom Hirschowitz, Xavier Leroy, J. B. Wells |
Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types. |
ESOP |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Java Bytecode Verification: Algorithms and Formalizations. |
J. Autom. Reasoning |
2003 |
DBLP DOI BibTeX RDF |
abstract interpretation, Java Virtual Machine, subroutines, dataflow analysis, bytecode verification |
| 1 | Cristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy |
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. |
GPCE |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Tom Hirschowitz, Xavier Leroy, J. B. Wells |
Compilation of extended recursion in call-by-value functional languages. |
PPDP |
2003 |
DBLP DOI BibTeX RDF |
compilation, semantics, recursion, functional languages |
| 1 | Xavier Leroy |
Computer Security from a Programming Language and Static Analysis Perspective. |
ESOP |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Bytecode verification on Java smart cards. |
Softw., Pract. Exper. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Grégoire, Xavier Leroy |
A compiled implementation of strong reduction. |
ICFP |
2002 |
DBLP DOI BibTeX RDF |
beta-equivalence, calculus of constructions, normalization by evaluation, strong reduction, virtual machine, abstract machine, Coq |
| 1 | Tom Hirschowitz, Xavier Leroy |
Mixin Modules in a Call-by-Value Setting. |
ESOP |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
On-Card Bytecode Verification for Java Card. |
E-smart |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Java Bytecode Verification: An Overview. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy, François Pessaux |
Type-based analysis of uncaught exceptions. |
ACM Trans. Program. Lang. Syst. |
2000 |
DBLP DOI BibTeX RDF |
rows, ML, polymorphism, type inference, exceptions, type and effect systems, SML, static debugging, caml |
| 1 | Xavier Leroy |
A modular module system. |
J. Funct. Program. |
2000 |
DBLP BibTeX RDF |
|
| 1 | Xavier Leroy, François Rouaix |
Security Properties of Typed Applets. |
Secure Internet Programming |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | François Pessaux, Xavier Leroy |
Type-Based Analysis of Uncaught Exceptions. |
POPL |
1999 |
DBLP DOI BibTeX RDF |
ML |
| 1 | Xavier Leroy, François Rouaix |
Security Properties of Typed Applets. |
POPL |
1998 |
DBLP DOI BibTeX RDF |
Java |
| 1 | Xavier Leroy |
Introduction. |
Types in Compilation |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy, Atsushi Ohori (eds.) |
Types in Compilation, Second International Workshop, TIC '98, Kyoto, Japan, March 25-27, 1998, Proceedings |
TIC |
1998 |
DBLP BibTeX RDF |
|
| 1 | 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. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
A Syntactic Theory of Type Generativity and Sharing. |
J. Funct. Program. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Applicative Functors and Fully Transparent Higher-Order Modules. |
POPL |
1995 |
DBLP DOI BibTeX RDF |
Standard ML |
| 1 | Xavier Leroy |
Manifest Types, Modules, and Separate Compilation. |
POPL |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy, Michel Mauny |
Dynamics in ML. |
J. Funct. Program. |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy, Pierre Weis |
Manuel de référence du langage CAML. |
|
1993 |
RDF |
|
| 1 | Pierre Weis, Xavier Leroy |
Le langage Caml. |
|
1993 |
RDF |
|
| 1 | Xavier Leroy |
Polymorphism by Name for References and Continuations. |
POPL |
1993 |
DBLP DOI BibTeX RDF |
ML |
| 1 | Damien Doligez, Xavier Leroy |
A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML. |
POPL |
1993 |
DBLP DOI BibTeX RDF |
LML |
| 1 | Xavier Leroy |
Unboxed Objects and Polymorphic Typing. |
POPL |
1992 |
DBLP DOI BibTeX RDF |
ML |
| 1 | Xavier Leroy, Pierre Weis |
Polymorphic Type Inference and Assignment. |
POPL |
1991 |
DBLP DOI BibTeX RDF |
ML |
| 1 | Xavier Leroy, Michel Mauny |
Dynamics in ML. |
FPCA |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
Efficient Data Representation in Polymorphic Languages. |
PLILP |
1990 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")