| Formal verification of a realistic compiler X Leroy Communications of the ACM 52 (7), 107-115, 2009 | 1823 | 2009 |
| Formal certification of a compiler back-end or: programming a compiler with a proof assistant X Leroy Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of …, 2006 | 986 | 2006 |
| A formally verified compiler back-end X Leroy Journal of Automated Reasoning 43, 363-446, 2009 | 748 | 2009 |
| Manifest types, modules, and separate compilation X Leroy Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of …, 1994 | 370 | 1994 |
| The ZINC experiment : an economical implementation of the ML language X Leroy INRIA, 1990 | 333 | 1990 |
| The Objective Caml system release 3.10: Documentation and user's manual X Leroy http://caml. inria. fr/, 2007 | 322* | 2007 |
| Unboxed objects and polymorphic typing X Leroy Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of …, 1992 | 312 | 1992 |
| A concurrent, generational garbage collector for a multithreaded implementation of ML D Doligez, X Leroy Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of …, 1993 | 302 | 1993 |
| Mechanized semantics for the Clight subset of the C language S Blazy, X Leroy Journal of Automated Reasoning 43 (3), 263-288, 2009 | 292 | 2009 |
| Program logics for certified compilers AW Appel Cambridge University Press, 2014 | 271 | 2014 |
| A compiled implementation of strong reduction B Grégoire, X Leroy Proceedings of the seventh ACM SIGPLAN international conference on …, 2002 | 268 | 2002 |
| The OCaml system release 5.1: Documentation and user's manual X Leroy, D Doligez, A Frisch, J Garrigue, D Rémy, KC Sivaramakrishnan, ... Inria, 2023 | 244* | 2023 |
| Coinductive big-step operational semantics X Leroy, H Grall Information and Computation 207 (2), 284-304, 2009 | 239 | 2009 |
| Formal verification of a C-like memory model and its uses for verifying program transformations X Leroy, S Blazy Journal of Automated Reasoning 41, 1-31, 2008 | 235 | 2008 |
| Formal verification of a C compiler front-end S Blazy, Z Dargaye, X Leroy FM 2006: Formal Methods: 14th International Symposium on Formal Methods …, 2006 | 234 | 2006 |
| Java bytecode verification: algorithms and formalizations X Leroy Journal of Automated Reasoning 30 (3), 235-269, 2003 | 234 | 2003 |
| A formally-verified C static analyzer JH Jourdan, V Laporte, S Blazy, X Leroy, D Pichardie Acm Sigplan Notices 50 (1), 247-259, 2015 | 222 | 2015 |
| The Objective Caml System, release 3. 08 X Leroy, D Doligez, J Garrigue, D Rmy, J Vouillon | 222 | 2004 |
| Managing the complexity of large free and open source package-based software distributions F Mancinelli, J Boender, R Di Cosmo, J Vouillon, B Durak, X Leroy, ... 21st IEEE/ACM International Conference on Automated Software Engineering …, 2006 | 221 | 2006 |
| Applicative functors and fully transparent higher-order modules X Leroy Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of …, 1995 | 212 | 1995 |
Damien DoligezChargé de recherches, InriaDirección de correo verificada de inria.fr
