Xavier Leroy
Titel
Zitiert von
Zitiert von
Jahr
Formal verification of a realistic compiler
X Leroy
Communications of the ACM 52 (7), 107-115, 2009
12382009
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
8472006
A formally verified compiler back-end
X Leroy
Journal of Automated Reasoning 43 (4), 363, 2009
5612009
Manifest types, modules, and separate compilation
X Leroy
Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of …, 1994
3601994
Unboxed objects and polymorphic typing
X Leroy
Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of …, 1992
2971992
The ZINC experiment : an economical implementation of the ML language
X Leroy
INRIA, 1990
2841990
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
2771993
Java bytecode verification: algorithms and formalizations
X Leroy
Journal of Automated Reasoning 30 (3-4), 235-269, 2003
2272003
A compiled implementation of strong reduction
B Grégoire, X Leroy
Proceedings of the seventh ACM SIGPLAN international conference on …, 2002
2272002
The Objective Caml System, release 3. 08
X Leroy, D Doligez, J Garrigue, D Rmy, J Vouillon
2172004
Formal verification of a C compiler front-end
S Blazy, Z Dargaye, X Leroy
International Symposium on Formal Methods, 460-475, 2006
2122006
Mechanized semantics for the Clight subset of the C language
S Blazy, X Leroy
Journal of Automated Reasoning 43 (3), 263-288, 2009
2072009
Coinductive big-step operational semantics
X Leroy, H Grall
Information and Computation 207 (2), 284-304, 2009
2032009
Applicative functors and fully transparent higher-order modules
X Leroy
Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of …, 1995
2021995
The Objective Caml system release 3.10: Documentation and user's manual
X Leroy
http://caml. inria. fr/, 2007
2012007
A modular module system
X Leroy
1822000
The OCaml system release 4.09: Documentation and user's manual
X Leroy, D Doligez, A Frisch, J Garrigue, D Rémy, J Vouillon
Inria, 2019
178*2019
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), 1-31, 2008
1762008
Type-based analysis of uncaught exceptions
F Pessaux, X Leroy
Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of …, 1999
173*1999
Program logics for certified compilers
AW Appel
Cambridge University Press, 2014
1702014
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20