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
