Xavier Leroy

Cited by

	All	Since 2016
Citations	11241	3366
h-index	53	26
i10-index	99	47

700

350

175

525

19921993199419951996199719981999200020012002200320042005200620072008200920102011201220132014201520162017201820192020202143 54 114 132 172 159 202 174 232 192 290 328 343 343 366 438 428 540 473 412 564 493 577 609 569 617 620 698 580 281

Co-authors

Damien DoligezChargé de recherches, InriaVerified email at inria.fr
Sandrine BlazyProfessor of Computer Science, University of RennesVerified email at irisa.fr
Roberto Di CosmoProfessor of Computer Science, University Paris DiderotVerified email at dicosmo.org
Tom HirschowitzCNRSVerified email at univ-smb.fr
Jacques-Henri JourdanUniversité Paris-Saclay, CNRS, Laboratoire de Recherche en InformatiqueVerified email at normalesup.org
Andrew W. AppelProfessor of Computer Science, Princeton UniversityVerified email at princeton.edu
Walid TahaHalmstad UniversityVerified email at hh.se
Gordon StewartAssistant Professor, Ohio UniversityVerified email at ohio.edu
Jean-Baptiste TristanBoston CollegeVerified email at oracle.com
Francois RouaixPrincipal Software Engineer, MicrosoftVerified email at rouaix.org
Christian FerdinandVerified email at absint.com
David PichardieProfessor, ENS Rennes, FranceVerified email at inria.fr
Marco DaneluttoProfessor, Dept. of Computer Science, Univ. of PisaVerified email at unipi.it
Marc PantelAssociate Professor in Computer Science, Université de ToulouseVerified email at enseeiht.fr
Guillaume MelquiondInria, University Paris SaclayVerified email at inria.fr
Sylvie BoldoInria, LRI, University Paris Sud, CNRSVerified email at inria.fr
Valentin RobertUniversity of California, San DiegoVerified email at cs.ucsd.edu
Robert DockinsPrinceton University

Xavier Leroy

Collège de France

Verified email at college-de-france.fr - Homepage

Programming languages Software verification Program proof Compilers Functional programming


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
Formal verification of a realistic compiler X Leroy Communications of the ACM 52 (7), 107-115, 2009	1304	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	867	2006
A formally verified compiler back-end X Leroy Journal of Automated Reasoning 43 (4), 363-446, 2009	584	2009
Manifest types, modules, and separate compilation X Leroy Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of …, 1994	358	1994
Unboxed objects and polymorphic typing X Leroy Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of …, 1992	301	1992
The ZINC experiment : an economical implementation of the ML language X Leroy INRIA, 1990	284	1990
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	283	1993
A compiled implementation of strong reduction B Grégoire, X Leroy Proceedings of the seventh ACM SIGPLAN international conference on …, 2002	232	2002
Java bytecode verification: algorithms and formalizations X Leroy Journal of Automated Reasoning 30 (3), 235-269, 2003	227	2003
The Objective Caml System, release 3. 08 X Leroy, D Doligez, J Garrigue, D Rmy, J Vouillon	221	2004
Mechanized semantics for the Clight subset of the C language S Blazy, X Leroy Journal of Automated Reasoning 43 (3), 263-288, 2009	218	2009
Formal verification of a C compiler front-end S Blazy, Z Dargaye, X Leroy International Symposium on Formal Methods, 460-475, 2006	213	2006
Coinductive big-step operational semantics X Leroy, H Grall Information and Computation 207 (2), 284-304, 2009	204	2009
The Objective Caml system release 3.10: Documentation and user's manual X Leroy http://caml. inria. fr/, 2007	202	2007
Applicative functors and fully transparent higher-order modules X Leroy Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of …, 1995	201	1995
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	183	2008
A modular module system X Leroy Journal of Functional Programming 10 (3), 269-303, 2000	181	2000
Program logics for certified compilers AW Appel, S Blazy, X Leroy, G Stewart Cambridge University Press, 2014	180	2014
The OCaml system release 3.12 X Leroy, D Doligez, A Frisch, J Garrigue, D Rémy, J Vouillon Institut National de Recherche en Informatique et en Automatique, 2011	180*	2011
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	176	2006

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Upload PDF

Follow this author

Cited by

Co-authors