Xavier Leroy
From MaRDI portal
List of research outcomes
This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!
| Publication | Date of Publication | Type |
|---|---|---|
| Efficient extensional binary tries Journal of Automated Reasoning | 2023-06-14 | Paper |
| Formal certification of a compiler back-end or: programming a compiler with a proof assistant Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2017-08-21 | Paper |
| A compiled implementation of strong reduction Proceedings of the seventh ACM SIGPLAN international conference on Functional programming | 2015-10-07 | Paper |
| A mechanized semantics for C++ object construction and destruction, with applications to resource management Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
| Verified compilation of floating-point computations Journal of Automated Reasoning | 2015-07-02 | Paper |
| A simple, verified validator for software pipelining Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-06-11 | Paper |
| Formal verification of translation validators Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
| Program logics for certified compilers | 2014-07-28 | Paper |
| Formal verification of object layout for C++ multiple inheritance Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-04-10 | Paper |
| Verified squared, does critical software deserve verified tools? Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-04-10 | Paper |
| A list-machine benchmark for mechanized metatheory (extended abstract) | 2014-01-10 | Paper |
| A formally-verified alias analysis Certified Programs and Proofs | 2013-04-19 | Paper |
| A list-machine benchmark for mechanized metatheory Journal of Automated Reasoning | 2013-04-17 | Paper |
| Validating LR(1) Parsers Programming Languages and Systems | 2012-06-22 | Paper |
| Mechanized semantics (available as arXiv preprint) | 2010-12-13 | Paper |
| A verified framework for higher-order uncurrying optimizations Higher-Order and Symbolic Computation | 2010-05-05 | Paper |
| Compilation of extended recursion in call-by-value functional languages Higher-Order and Symbolic Computation | 2010-03-05 | Paper |
| Mechanized semantics for the clight subset of the C language Journal of Automated Reasoning | 2010-01-25 | Paper |
| A formally verified compiler back-end Journal of Automated Reasoning | 2010-01-25 | Paper |
| Coinductive big-step operational semantics Information and Computation | 2009-04-14 | Paper |
| Formal verification of a C-like memory model and its uses for verifying program transformations Journal of Automated Reasoning | 2008-09-10 | Paper |
| Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves Journal of Automated Reasoning | 2008-06-11 | Paper |
| Mechanized Verification of CPS Transformations Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
| Programming Languages and Systems Lecture Notes in Computer Science | 2007-09-28 | Paper |
| Programming Languages and Systems Lecture Notes in Computer Science | 2007-05-02 | Paper |
| Types for Proofs and Programs Lecture Notes in Computer Science | 2006-11-13 | Paper |
| scientific article; zbMATH DE number 2087534 (Why is no real title available?) | 2004-08-11 | Paper |
| Java bytecode verification: Algorithms and formalizations Journal of Automated Reasoning | 2003-09-09 | Paper |
| scientific article; zbMATH DE number 1956541 (Why is no real title available?) | 2003-07-30 | Paper |
| Bytecode verification on Java smart cards Software: Practice and Experience | 2003-02-04 | Paper |
| scientific article; zbMATH DE number 1857507 (Why is no real title available?) | 2003-02-02 | Paper |
| scientific article; zbMATH DE number 1798185 (Why is no real title available?) | 2002-11-04 | Paper |
| A modular module system Journal of Functional Programming | 2000-10-10 | Paper |
| A syntactic theory of type generativity and sharing Journal of Functional Programming | 1997-03-18 | Paper |
Research outcomes over time
This page was built for person: Xavier Leroy
