Xavier Leroy

Available identifiers

zbMath Open leroy.xavierMaRDI QIDQ848738

List of research outcomes

Publication	Date of Publication	Type
Efficient extensional binary tries	2023-06-14	Paper
Formal certification of a compiler back-end or	2017-08-21	Paper
A compiled implementation of strong reduction	2015-10-07	Paper
A mechanized semantics for C++ object construction and destruction, with applications to resource management	2015-09-11	Paper
Verified compilation of floating-point computations	2015-07-02	Paper
A simple, verified validator for software pipelining	2015-06-11	Paper
Formal verification of translation validators	2014-09-12	Paper
Program Logics for Certified Compilers	2014-07-28	Paper
Formal verification of object layout for c++ multiple inheritance	2014-04-10	Paper
Verified squared	2014-04-10	Paper
A list-machine benchmark for mechanized metatheory (extended abstract)	2014-01-10	Paper
A Formally-Verified Alias Analysis	2013-04-19	Paper
A list-machine benchmark for mechanized metatheory	2013-04-17	Paper
Validating LR(1) Parsers	2012-06-22	Paper
Mechanized semantics	2010-12-13	Paper
A verified framework for higher-order uncurrying optimizations	2010-05-05	Paper
Compilation of extended recursion in call-by-value functional languages	2010-03-05	Paper
Mechanized semantics for the clight subset of the C language	2010-01-25	Paper
A formally verified compiler back-end	2010-01-25	Paper
Coinductive big-step operational semantics	2009-04-14	Paper
Formal verification of a C-like memory model and its uses for verifying program transformations	2008-09-10	Paper
Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves	2008-06-11	Paper
Mechanized Verification of CPS Transformations	2008-05-15	Paper
Programming Languages and Systems	2007-09-28	Paper
Programming Languages and Systems	2007-05-02	Paper
Types for Proofs and Programs	2006-11-13	Paper
https://portal.mardi4nfdi.de/entity/Q4738342	2004-08-11	Paper
Java bytecode verification: Algorithms and formalizations	2003-09-09	Paper
https://portal.mardi4nfdi.de/entity/Q4417878	2003-07-30	Paper
Bytecode verification on Java smart cards	2003-02-04	Paper
https://portal.mardi4nfdi.de/entity/Q4788555	2003-02-02	Paper
https://portal.mardi4nfdi.de/entity/Q4553258	2002-11-04	Paper
A modular module system	2000-10-10	Paper
A syntactic theory of type generativity and sharing	1997-03-18	Paper

Research outcomes over time

This page was built for person: Xavier Leroy