@inproceedings{Leroy95,
  title = {Applicative Functors and Fully Transparent Higher-Order Modules},
  author = {Xavier Leroy},
  year = {1995},
  researchr = {https://researchr.org/publication/Leroy95},
  cites = {0},
  citedby = {0},
  pages = {142-153},
  booktitle = {POPL},
}

@inproceedings{TristanL09,
  title = {Verified validation of lazy code motion},
  author = {Jean-Baptiste Tristan and Xavier Leroy},
  year = {2009},
  doi = {10.1145/1542476.1542512},
  url = {http://doi.acm.org/10.1145/1542476.1542512},
  tags = {laziness},
  researchr = {https://researchr.org/publication/TristanL09},
  cites = {0},
  citedby = {0},
  pages = {316-326},
  booktitle = {PLDI},
}

@inproceedings{TristanL08,
  title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
  author = {Jean-Baptiste Tristan and Xavier Leroy},
  year = {2008},
  doi = {10.1145/1328438.1328444},
  url = {http://doi.acm.org/10.1145/1328438.1328444},
  tags = {optimization, translation, case study},
  researchr = {https://researchr.org/publication/TristanL08},
  cites = {0},
  citedby = {0},
  pages = {17-27},
  booktitle = {POPL},
}

@article{Leroy03-0,
  title = {Java Bytecode Verification: Algorithms and Formalizations},
  author = {Xavier Leroy},
  year = {2003},
  doi = {10.1023/A:1025055424017},
  url = {http://dx.doi.org/10.1023/A:1025055424017},
  tags = {Java},
  researchr = {https://researchr.org/publication/Leroy03-0},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {30},
  number = {3-4},
  pages = {235-269},
}

@book{0072364,
  title = {Manuel de référence du langage CAML},
  author = {Xavier Leroy and Pierre Weis},
  year = {1993},
  researchr = {https://researchr.org/publication/0072364},
  cites = {0},
  citedby = {0},
  publisher = {InterEditions},
  isbn = {978-2-7296-0492-9},
}

@inproceedings{Leroy14-0,
  title = {Formal Proofs of Code Generation and Verification Tools},
  author = {Xavier Leroy},
  year = {2014},
  doi = {10.1007/978-3-319-10431-7_1},
  url = {http://dx.doi.org/10.1007/978-3-319-10431-7_1},
  researchr = {https://researchr.org/publication/Leroy14-0},
  cites = {0},
  citedby = {0},
  pages = {1-4},
  booktitle = {SEFM},
}

@article{LeroyF09,
  title = {Editorial},
  author = {Xavier Leroy and Matthias Felleisen},
  year = {2009},
  doi = {10.1017/S095679680999013X},
  url = {http://dx.doi.org/10.1017/S095679680999013X},
  researchr = {https://researchr.org/publication/LeroyF09},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {19},
  number = {5},
  pages = {489-490},
}

@article{BoldoJLM15,
  title = {Verified Compilation of Floating-Point Computations},
  author = {Sylvie Boldo and Jacques-Henri Jourdan and Xavier Leroy and Guillaume Melquiond},
  year = {2015},
  doi = {10.1007/s10817-014-9317-x},
  url = {http://dx.doi.org/10.1007/s10817-014-9317-x},
  researchr = {https://researchr.org/publication/BoldoJLM15},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {54},
  number = {2},
  pages = {135-163},
}

@inproceedings{LeroyR98,
  title = {Security Properties of Typed Applets},
  author = {Xavier Leroy and François Rouaix},
  year = {1998},
  doi = {10.1145/268946.268979},
  url = {http://doi.acm.org/10.1145/268946.268979},
  tags = {security},
  researchr = {https://researchr.org/publication/LeroyR98},
  cites = {0},
  citedby = {0},
  pages = {391-403},
  booktitle = {POPL},
}

@inproceedings{HirschowitzLW04,
  title = {Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types},
  author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2986&spage=64},
  tags = {semantics},
  researchr = {https://researchr.org/publication/HirschowitzLW04},
  cites = {0},
  citedby = {0},
  pages = {64-78},
  booktitle = {ESOP},
}

@article{DargayeL09,
  title = {A verified framework for higher-order uncurrying optimizations},
  author = {Zaynah Dargaye and Xavier Leroy},
  year = {2009},
  doi = {10.1007/s10990-010-9050-z},
  url = {http://dx.doi.org/10.1007/s10990-010-9050-z},
  tags = {optimization},
  researchr = {https://researchr.org/publication/DargayeL09},
  cites = {0},
  citedby = {0},
  journal = {lisp},
  volume = {22},
  number = {3},
  pages = {199-231},
}

@inproceedings{Leroy92,
  title = {Unboxed Objects and Polymorphic Typing},
  author = {Xavier Leroy},
  year = {1992},
  tags = {meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/Leroy92},
  cites = {0},
  citedby = {0},
  pages = {177-188},
  booktitle = {POPL},
}

@article{HartelFAABBCFGGHHIJKLLLLRSTTTWWW96,
  title = {Benchmarking Implementations of Functional Languages with  Pseudoknot , a Float-Intensive Benchmark},
  author = {Pieter H. Hartel and Marc Feeley and Martin Alt and Lennart Augustsson and Peter Baumann and Marcel Beemster and Emmanuel Chailloux and Christine H. Flood and Wolfgang Grieskamp and John H. G. van Groningen and Kevin Hammond and Bogumil Hausman and Melody Y. Ivory and Richard E. Jones and Jasper Kamperman and Peter Lee and Xavier Leroy and Rafael Dueire Lins and Sandra Loosemore and Niklas Röjemo and Manuel Serrano and Jean-Pierre Talpin and Jon Thackray and Stephen Thomas and Pum Walters and Pierre Weis and Peter Wentworth},
  year = {1996},
  researchr = {https://researchr.org/publication/HartelFAABBCFGGHHIJKLLLLRSTTTWWW96},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {6},
  number = {4},
  pages = {621-655},
}

@article{Leroy09,
  title = {Formal verification of a realistic compiler},
  author = {Xavier Leroy},
  year = {2009},
  doi = {10.1145/1538788.1538814},
  url = {http://doi.acm.org/10.1145/1538788.1538814},
  tags = {programming languages, semantics, semantic preservation, proof assistant, CompCert, program verification, formal semantics, type soundness, source-to-source, C++, compiler, programming, context-aware, open-source},
  researchr = {https://researchr.org/publication/Leroy09},
  cites = {0},
  citedby = {0},
  journal = {CACM},
  volume = {52},
  number = {7},
  pages = {107-115},
}

@inproceedings{Leroy90,
  title = {Efficient Data Representation in Polymorphic Languages},
  author = {Xavier Leroy},
  year = {1990},
  tags = {data-flow language, data-flow},
  researchr = {https://researchr.org/publication/Leroy90},
  cites = {0},
  citedby = {0},
  pages = {255-276},
  booktitle = {plilp},
}

@inproceedings{BoldoJLM13,
  title = {A Formally-Verified C Compiler Supporting Floating-Point Arithmetic},
  author = {Sylvie Boldo and Jacques-Henri Jourdan and Xavier Leroy and Guillaume Melquiond},
  year = {2013},
  doi = {10.1109/ARITH.2013.30},
  url = {http://doi.ieeecomputersociety.org/10.1109/ARITH.2013.30},
  researchr = {https://researchr.org/publication/BoldoJLM13},
  cites = {0},
  citedby = {0},
  pages = {107-115},
  booktitle = {arith},
}

@manual{leroy2020ocaml,
  title = {The {OCaml} system release 4.10},
  author = {Xavier Leroy and Damien Doligez and Alain Frisch and Garrigue, Jacques and Didier Rémy and Jérôme Vouillon},
  year = {2020},
  month = {February},
  url = {https://ocaml.org/releases/4.10/htmlman/index.html},
  researchr = {https://researchr.org/publication/leroy2020ocaml},
  cites = {0},
  citedby = {0},
}

@article{HirschowitzL05,
  title = {Mixin modules in a call-by-value setting},
  author = {Tom Hirschowitz and Xavier Leroy},
  year = {2005},
  doi = {10.1145/1086642.1086644},
  url = {http://doi.acm.org/10.1145/1086642.1086644},
  researchr = {https://researchr.org/publication/HirschowitzL05},
  cites = {0},
  citedby = {0},
  journal = {TOPLAS},
  volume = {27},
  number = {5},
  pages = {857-881},
}

@article{LeroyG09,
  title = {Coinductive big-step operational semantics},
  author = {Xavier Leroy and Hervé Grall},
  year = {2009},
  doi = {10.1016/j.ic.2007.12.004},
  url = {http://dx.doi.org/10.1016/j.ic.2007.12.004},
  tags = {semantics, discovery, proof assistant, CompCert, formal semantics, type soundness, compiler, operational semantics, natural semantics},
  researchr = {https://researchr.org/publication/LeroyG09},
  cites = {0},
  citedby = {0},
  journal = {iandc},
  volume = {207},
  number = {2},
  pages = {284-304},
}

@inproceedings{JourdanPL12,
  title = {Validating LR(1) Parsers},
  author = {Jacques-Henri Jourdan and François Pottier and Xavier Leroy},
  year = {2012},
  doi = {10.1007/978-3-642-28869-2_20},
  url = {http://dx.doi.org/10.1007/978-3-642-28869-2_20},
  researchr = {https://researchr.org/publication/JourdanPL12},
  cites = {0},
  citedby = {0},
  pages = {397-416},
  booktitle = {ESOP},
}

@article{Leroy11-0,
  title = {Safety first!: technical perspective},
  author = {Xavier Leroy},
  year = {2011},
  doi = {10.1145/2043174.2043196},
  url = {http://doi.acm.org/10.1145/2043174.2043196},
  researchr = {https://researchr.org/publication/Leroy11-0},
  cites = {0},
  citedby = {0},
  journal = {CACM},
  volume = {54},
  number = {12},
  pages = {122},
}

@inproceedings{Leroy01,
  title = {Java Bytecode Verification: An Overview},
  author = {Xavier Leroy},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2102/21020265.htm},
  tags = {Java},
  researchr = {https://researchr.org/publication/Leroy01},
  cites = {0},
  citedby = {0},
  pages = {265-285},
  booktitle = {cav},
}

@inproceedings{RideauL10,
  title = {Validating Register Allocation and Spilling},
  author = {Silvain Rideau and Xavier Leroy},
  year = {2010},
  doi = {10.1007/978-3-642-11970-5_13},
  url = {http://dx.doi.org/10.1007/978-3-642-11970-5_13},
  researchr = {https://researchr.org/publication/RideauL10},
  cites = {0},
  citedby = {0},
  pages = {224-243},
  booktitle = {CC},
}

@article{Leroy96,
  title = {A Syntactic Theory of Type Generativity and Sharing},
  author = {Xavier Leroy},
  year = {1996},
  tags = {type theory},
  researchr = {https://researchr.org/publication/Leroy96},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {6},
  number = {5},
  pages = {667-698},
}

@article{RideauSL08,
  title = {Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves},
  author = {Laurence Rideau and Bernard P. Serpette and Xavier Leroy},
  year = {2008},
  doi = {10.1007/s10817-007-9096-8},
  url = {http://dx.doi.org/10.1007/s10817-007-9096-8},
  researchr = {https://researchr.org/publication/RideauSL08},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {40},
  number = {4},
  pages = {307-326},
}

@article{Leroy09-0,
  title = {Editorial},
  author = {Xavier Leroy},
  year = {2009},
  doi = {10.1017/S0956796809007187},
  url = {http://dx.doi.org/10.1017/S0956796809007187},
  researchr = {https://researchr.org/publication/Leroy09-0},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {19},
  number = {2},
  pages = {143},
}

@inproceedings{JourdanLBLP15,
  title = {A Formally-Verified C Static Analyzer},
  author = {Jacques-Henri Jourdan and Vincent Laporte and Sandrine Blazy and Xavier Leroy and David Pichardie},
  year = {2015},
  doi = {10.1145/2676726.2676966},
  url = {http://doi.acm.org/10.1145/2676726.2676966},
  researchr = {https://researchr.org/publication/JourdanLBLP15},
  cites = {0},
  citedby = {0},
  pages = {247-259},
  booktitle = {POPL},
}

@inproceedings{Leroy07,
  title = {Formal verification of an optimizing compiler},
  author = {Xavier Leroy},
  year = {2007},
  doi = {10.1109/MEMCOD.2007.371254},
  url = {http://dx.doi.org/10.1109/MEMCOD.2007.371254},
  tags = {optimization, compiler},
  researchr = {https://researchr.org/publication/Leroy07},
  cites = {0},
  citedby = {0},
  pages = {25},
  booktitle = {memocode},
}

@article{AppelDL12,
  title = {A List-Machine Benchmark for Mechanized Metatheory},
  author = {Andrew W. Appel and Robert Dockins and Xavier Leroy},
  year = {2012},
  doi = {10.1007/s10817-011-9226-1},
  url = {http://dx.doi.org/10.1007/s10817-011-9226-1},
  researchr = {https://researchr.org/publication/AppelDL12},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {49},
  number = {3},
  pages = {453-491},
}

@inproceedings{Leroy06-POPL,
  title = {Formal certification of a compiler back-end or: programming a compiler with a proof assistant},
  author = {Xavier Leroy},
  year = {2006},
  doi = {10.1145/1111037.1111042},
  url = {http://doi.acm.org/10.1145/1111037.1111042},
  tags = {proof assistant, certification, compiler, programming},
  researchr = {https://researchr.org/publication/Leroy06-POPL},
  cites = {0},
  citedby = {1},
  pages = {42-54},
  booktitle = {POPL},
}

@inproceedings{Leroy12,
  title = {Mechanized Semantics for Compiler Verification},
  author = {Xavier Leroy},
  year = {2012},
  doi = {10.1007/978-3-642-35182-2_27},
  url = {http://dx.doi.org/10.1007/978-3-642-35182-2_27},
  researchr = {https://researchr.org/publication/Leroy12},
  cites = {0},
  citedby = {0},
  pages = {386-388},
  booktitle = {aplas},
}

@inproceedings{Leroy12-0,
  title = {Mechanized Semantics for Compiler Verification},
  author = {Xavier Leroy},
  year = {2012},
  doi = {10.1007/978-3-642-35308-6_2},
  url = {http://dx.doi.org/10.1007/978-3-642-35308-6_2},
  researchr = {https://researchr.org/publication/Leroy12-0},
  cites = {0},
  citedby = {0},
  pages = {4-6},
  booktitle = {CPP},
}

@inproceedings{Leroy07:0,
  title = {Formal Verification of an Optimizing Compiler},
  author = {Xavier Leroy},
  year = {2007},
  doi = {10.1007/978-3-540-73449-9_1},
  url = {http://dx.doi.org/10.1007/978-3-540-73449-9_1},
  tags = {optimization, compiler},
  researchr = {https://researchr.org/publication/Leroy07%3A0},
  cites = {0},
  citedby = {0},
  pages = {1},
  booktitle = {RTA},
}

@inproceedings{Leroy98,
  title = {Introduction},
  author = {Xavier Leroy},
  year = {1998},
  url = {http://link.springer.de/link/service/series/0558/bibs/1473/14730001.htm},
  researchr = {https://researchr.org/publication/Leroy98},
  cites = {0},
  citedby = {0},
  pages = {1-8},
  booktitle = {tic},
}

@article{BlazyL09,
  title = {Mechanized Semantics for the {Clight} Subset of the {C} Language},
  author = {Sandrine Blazy and Xavier Leroy},
  year = {2009},
  doi = {10.1007/s10817-009-9148-3},
  url = {http://dx.doi.org/10.1007/s10817-009-9148-3},
  tags = {semantics, CompCert, formal semantics, C++, natural semantics},
  researchr = {https://researchr.org/publication/BlazyL09},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {43},
  number = {3},
  pages = {263-288},
}

@article{TolmachL11,
  title = {Special Issue Dedicated to ICFP 2009 Editorial},
  author = {Andrew P. Tolmach and Xavier Leroy},
  year = {2011},
  doi = {10.1017/S0956796811000190},
  url = {http://dx.doi.org/10.1017/S0956796811000190},
  researchr = {https://researchr.org/publication/TolmachL11},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {21},
  number = {4-5},
  pages = {331-332},
}

@inproceedings{BlazyL05,
  title = {Formal Verification of a Memory Model for ::::C::::-Like Imperative Languages},
  author = {Sandrine Blazy and Xavier Leroy},
  year = {2005},
  doi = {10.1007/11576280_20},
  url = {http://dx.doi.org/10.1007/11576280_20},
  tags = {modeling language, language modeling, C++},
  researchr = {https://researchr.org/publication/BlazyL05},
  cites = {0},
  citedby = {0},
  pages = {280-299},
  booktitle = {icfem},
}

@inproceedings{Leroy93,
  title = {Polymorphism by Name for References and Continuations},
  author = {Xavier Leroy},
  year = {1993},
  researchr = {https://researchr.org/publication/Leroy93},
  cites = {0},
  citedby = {0},
  pages = {220-231},
  booktitle = {POPL},
}

@article{BentonL06,
  title = {Preface},
  author = {Nick Benton and Xavier Leroy},
  year = {2006},
  doi = {10.1016/j.entcs.2005.11.037},
  url = {http://dx.doi.org/10.1016/j.entcs.2005.11.037},
  researchr = {https://researchr.org/publication/BentonL06},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {148},
  number = {2},
  pages = {1-2},
}

@inproceedings{954190,
  title = {Implementing multi-stage languages using ASTs, Gensym, and reflection},
  author = {Calcagno, Cristiano and Walid Taha and Huang, Liwen and Xavier Leroy},
  year = {2003},
  tags = {reflection},
  researchr = {https://researchr.org/publication/954190},
  cites = {0},
  citedby = {0},
  booktitle = {GPCE '03: Proceedings of the 2nd international conference on Generative programming and component engineering},
}

@inproceedings{MancinelliBCVDLT06,
  title = {Managing the Complexity of Large Free and Open Source Package-Based Software Distributions},
  author = {Fabio Mancinelli and Jaap Boender and Roberto Di Cosmo and Jérôme Vouillon and Berke Durak and Xavier Leroy and Ralf Treinen},
  year = {2006},
  doi = {10.1109/ASE.2006.49},
  url = {http://doi.ieeecomputersociety.org/10.1109/ASE.2006.49},
  tags = {rule-based, source-to-source, peer-to-peer, open-source},
  researchr = {https://researchr.org/publication/MancinelliBCVDLT06},
  cites = {0},
  citedby = {0},
  pages = {199-208},
  booktitle = {ASE},
}

@inproceedings{LeroyM91,
  title = {Dynamics in ML},
  author = {Xavier Leroy and Michel Mauny},
  year = {1991},
  researchr = {https://researchr.org/publication/LeroyM91},
  cites = {0},
  citedby = {0},
  pages = {406-426},
  booktitle = {fpca},
}

@inproceedings{BertotGL04,
  title = {A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis},
  author = {Yves Bertot and Benjamin Grégoire and Xavier Leroy},
  year = {2004},
  doi = {10.1007/11617990_5},
  url = {http://dx.doi.org/10.1007/11617990_5},
  tags = {optimization, rule-based, analysis, compiler, systematic-approach},
  researchr = {https://researchr.org/publication/BertotGL04},
  cites = {0},
  citedby = {0},
  pages = {66-81},
  booktitle = {TYPES},
}

@article{HirschowitzLW09,
  title = {Compilation of extended recursion in call-by-value functional languages},
  author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells},
  year = {2009},
  doi = {10.1007/s10990-009-9042-z},
  url = {http://dx.doi.org/10.1007/s10990-009-9042-z},
  researchr = {https://researchr.org/publication/HirschowitzLW09},
  cites = {0},
  citedby = {0},
  journal = {lisp},
  volume = {22},
  number = {1},
  pages = {3-66},
}

@article{LeroyB08,
  title = {Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations},
  author = {Xavier Leroy and Sandrine Blazy},
  year = {2008},
  doi = {10.1007/s10817-008-9099-0},
  url = {http://dx.doi.org/10.1007/s10817-008-9099-0},
  tags = {model-to-model transformation, meta programming, program verification, meta-model, source-to-source, C++, model transformation, Meta-Environment, transformation, program transformation},
  researchr = {https://researchr.org/publication/LeroyB08},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {41},
  number = {1},
  pages = {1-31},
}

@inproceedings{BlazyDL06,
  title = {Formal Verification of a {C} Compiler Front-End},
  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
  year = {2006},
  doi = {10.1007/11813040_31},
  url = {http://dx.doi.org/10.1007/11813040_31},
  tags = {C++, compiler},
  researchr = {https://researchr.org/publication/BlazyDL06},
  cites = {0},
  citedby = {1},
  pages = {460-475},
  booktitle = {FM},
}

@inproceedings{Leroy11,
  title = {Formally verifying a compiler: Why? How? How far?},
  author = {Xavier Leroy},
  year = {2011},
  doi = {10.1109/CGO.2011.5764668},
  url = {http://dx.doi.org/10.1109/CGO.2011.5764668},
  tags = {compiler},
  researchr = {https://researchr.org/publication/Leroy11},
  cites = {0},
  citedby = {0},
  booktitle = {CGO},
}

@article{Leroy-JAR-2009,
  title = {A Formally Verified Compiler Back-end},
  author = {Xavier Leroy},
  year = {2009},
  doi = {10.1007/s10817-009-9155-4},
  url = {http://dx.doi.org/10.1007/s10817-009-9155-4},
  tags = {programming languages, proof assistant, program verification, source-to-source, certification, compiler, programming, context-aware, open-source},
  researchr = {https://researchr.org/publication/Leroy-JAR-2009},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {43},
  number = {4},
  pages = {363-446},
}

@inproceedings{Leroy14-1,
  title = {Compiler verification for fun and profit},
  author = {Xavier Leroy},
  year = {2014},
  doi = {10.1109/FMCAD.2014.6987587},
  url = {http://dx.doi.org/10.1109/FMCAD.2014.6987587},
  researchr = {https://researchr.org/publication/Leroy14-1},
  cites = {0},
  citedby = {0},
  pages = {9},
  booktitle = {FMCAD},
}

@inproceedings{FrancaFLPS11,
  title = {Towards Formally Verified Optimizing Compilation in Flight Control Software},
  author = {Ricardo Bedin França and Denis Favre-Felix and Xavier Leroy and Marc Pantel and Jean Souyris},
  year = {2011},
  doi = {10.4230/OASIcs.PPES.2011.59},
  url = {http://dx.doi.org/10.4230/OASIcs.PPES.2011.59},
  tags = {optimization},
  researchr = {https://researchr.org/publication/FrancaFLPS11},
  cites = {0},
  citedby = {0},
  pages = {59-68},
  booktitle = {date},
}

@book{0072363,
  title = {Le langage Caml},
  author = {Pierre Weis and Xavier Leroy},
  year = {1993},
  researchr = {https://researchr.org/publication/0072363},
  cites = {0},
  citedby = {0},
  publisher = {InterEditions},
  isbn = {978-2-7296-0493-6},
}

@article{Leroy02,
  title = {Bytecode verification on Java smart cards},
  author = {Xavier Leroy},
  year = {2002},
  tags = {Java},
  researchr = {https://researchr.org/publication/Leroy02},
  cites = {0},
  citedby = {0},
  journal = {SPE},
  volume = {32},
  number = {4},
  pages = {319-340},
}

@article{LeroyP00,
  title = {Type-based analysis of uncaught exceptions},
  author = {Xavier Leroy and François Pessaux},
  year = {2000},
  doi = {10.1145/349214.349230},
  url = {http://doi.acm.org/10.1145/349214.349230},
  tags = {rule-based, exceptions, analysis},
  researchr = {https://researchr.org/publication/LeroyP00},
  cites = {0},
  citedby = {0},
  journal = {TOPLAS},
  volume = {22},
  number = {2},
  pages = {340-377},
}

@inproceedings{Leroy94,
  title = {Manifest Types, Modules, and Separate Compilation},
  author = {Xavier Leroy},
  year = {1994},
  doi = {10.1145/174675.176926},
  researchr = {https://researchr.org/publication/Leroy94},
  cites = {0},
  citedby = {0},
  pages = {109-122},
  booktitle = {POPL},
}

@inproceedings{Leroy06,
  title = {Coinductive Big-Step Operational Semantics},
  author = {Xavier Leroy},
  year = {2006},
  doi = {10.1007/11693024_5},
  url = {http://dx.doi.org/10.1007/11693024_5},
  tags = {semantics, type soundness, compiler, operational semantics},
  researchr = {https://researchr.org/publication/Leroy06},
  cites = {0},
  citedby = {0},
  pages = {54-68},
  booktitle = {ESOP},
}

@inproceedings{RamananandroRL12,
  title = {A mechanized semantics for C++ object construction and destruction, with applications to resource management},
  author = {Tahina Ramananandro and Gabriel Dos Reis and Xavier Leroy},
  year = {2012},
  doi = {10.1145/2103656.2103718},
  url = {http://doi.acm.org/10.1145/2103656.2103718},
  researchr = {https://researchr.org/publication/RamananandroRL12},
  cites = {0},
  citedby = {0},
  pages = {521-532},
  booktitle = {POPL},
}

@inproceedings{Leroy03,
  title = {Computer Security from a Programming Language and Static Analysis Perspective},
  author = {Xavier Leroy},
  year = {2003},
  url = {http://link.springer.de/link/service/series/0558/bibs/2618/26180001.htm},
  tags = {programming languages, program analysis, analysis, static analysis, security, programming},
  researchr = {https://researchr.org/publication/Leroy03},
  cites = {0},
  citedby = {0},
  pages = {1-9},
  booktitle = {ESOP},
}

@incollection{Leroy10,
  title = {Mechanized semantics - with applications to program proof and compiler verification},
  author = {Xavier Leroy},
  year = {2010},
  doi = {10.3233/978-1-60750-100-8-195},
  url = {http://dx.doi.org/10.3233/978-1-60750-100-8-195},
  researchr = {https://researchr.org/publication/Leroy10},
  cites = {0},
  citedby = {0},
  pages = {195-224},
  booktitle = {Logics and Languages for Reliability and Security},
  editor = {Javier Esparza and Bernd Spanfelner and Orna Grumberg},
  volume = {25},
  series = {NATO Science for Peace and Security Series - D: Information and Communication Security},
  publisher = {IOS Press},
  isbn = {978-1-60750-099-5},
}

@inproceedings{LeroyW91,
  title = {Polymorphic Type Inference and Assignment},
  author = {Xavier Leroy and Pierre Weis},
  year = {1991},
  tags = {type inference},
  researchr = {https://researchr.org/publication/LeroyW91},
  cites = {0},
  citedby = {0},
  pages = {291-302},
  booktitle = {POPL},
}

@inproceedings{RamananandroRL11,
  title = {Formal verification of object layout for c++ multiple inheritance},
  author = {Tahina Ramananandro and Gabriel Dos Reis and Xavier Leroy},
  year = {2011},
  doi = {10.1145/1926385.1926395},
  url = {http://doi.acm.org/10.1145/1926385.1926395},
  tags = {layout, meta-model, C++, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/RamananandroRL11},
  cites = {0},
  citedby = {0},
  pages = {67-80},
  booktitle = {POPL},
}

@inproceedings{LeroyR99,
  title = {Security Properties of Typed Applets},
  author = {Xavier Leroy and François Rouaix},
  year = {1999},
  tags = {security},
  researchr = {https://researchr.org/publication/LeroyR99},
  cites = {0},
  citedby = {0},
  pages = {147-182},
  booktitle = {ECOOPW},
}

@article{LeroyM93,
  title = {Dynamics in ML},
  author = {Xavier Leroy and Michel Mauny},
  year = {1993},
  researchr = {https://researchr.org/publication/LeroyM93},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {3},
  number = {4},
  pages = {431-463},
}

@inproceedings{Leroy01:0,
  title = {On-Card Bytecode Verification for Java Card},
  author = {Xavier Leroy},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2140/21400150.htm},
  tags = {Java},
  researchr = {https://researchr.org/publication/Leroy01%3A0},
  cites = {0},
  citedby = {0},
  pages = {150-164},
  booktitle = {esmart},
}

@inproceedings{RobertL12,
  title = {A Formally-Verified Alias Analysis},
  author = {Valentin Robert and Xavier Leroy},
  year = {2012},
  doi = {10.1007/978-3-642-35308-6_5},
  url = {http://dx.doi.org/10.1007/978-3-642-35308-6_5},
  researchr = {https://researchr.org/publication/RobertL12},
  cites = {0},
  citedby = {0},
  pages = {11-26},
  booktitle = {CPP},
}

@inproceedings{DargayeL07,
  title = {Mechanized Verification of CPS Transformations},
  author = {Zaynah Dargaye and Xavier Leroy},
  year = {2007},
  doi = {10.1007/978-3-540-75560-9_17},
  url = {http://dx.doi.org/10.1007/978-3-540-75560-9_17},
  tags = {transformation},
  researchr = {https://researchr.org/publication/DargayeL07},
  cites = {0},
  citedby = {0},
  pages = {211-225},
  booktitle = {lpar},
}

@article{AppelL07,
  title = {A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract)},
  author = {Andrew W. Appel and Xavier Leroy},
  year = {2007},
  doi = {10.1016/j.entcs.2007.01.020},
  url = {http://dx.doi.org/10.1016/j.entcs.2007.01.020},
  tags = {metatheory, abstract machine},
  researchr = {https://researchr.org/publication/AppelL07},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {174},
  number = {5},
  pages = {95-108},
}

@inproceedings{CalcagnoTHL03,
  title = {Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection},
  author = {Cristiano Calcagno and Walid Taha and Liwen Huang and Xavier Leroy},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2830&spage=57},
  tags = {reflection},
  researchr = {https://researchr.org/publication/CalcagnoTHL03},
  cites = {0},
  citedby = {1},
  pages = {57-76},
  booktitle = {GPCE},
}

@inproceedings{TristanL10,
  title = {A simple, verified validator for software pipelining},
  author = {Jean-Baptiste Tristan and Xavier Leroy},
  year = {2010},
  doi = {10.1145/1706299.1706311},
  url = {http://doi.acm.org/10.1145/1706299.1706311},
  researchr = {https://researchr.org/publication/TristanL10},
  cites = {0},
  citedby = {0},
  pages = {83-92},
  booktitle = {POPL},
}

@inproceedings{DoligezL93,
  title = {A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML},
  author = {Damien Doligez and Xavier Leroy},
  year = {1993},
  researchr = {https://researchr.org/publication/DoligezL93},
  cites = {0},
  citedby = {0},
  pages = {113-123},
  booktitle = {POPL},
}

@inproceedings{HirschowitzLW03,
  title = {Compilation of extended recursion in call-by-value functional languages},
  author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells},
  year = {2003},
  doi = {10.1145/888251.888267},
  url = {http://doi.acm.org/10.1145/888251.888267},
  researchr = {https://researchr.org/publication/HirschowitzLW03},
  cites = {0},
  citedby = {0},
  pages = {160-171},
  booktitle = {ppdp},
}

@inproceedings{GregoireL02,
  title = {A compiled implementation of strong reduction},
  author = {Benjamin Grégoire and Xavier Leroy},
  year = {2002},
  doi = {10.1145/581478.581501},
  url = {http://doi.acm.org/10.1145/581478.581501},
  tags = {compiler},
  researchr = {https://researchr.org/publication/GregoireL02},
  cites = {0},
  citedby = {0},
  pages = {235-246},
  booktitle = {ICFP},
}

@inproceedings{KrebbersLW14,
  title = {Formal C Semantics: CompCert and the C Standard},
  author = {Robbert Krebbers and Xavier Leroy and Freek Wiedijk},
  year = {2014},
  doi = {10.1007/978-3-319-08970-6_36},
  url = {http://dx.doi.org/10.1007/978-3-319-08970-6_36},
  researchr = {https://researchr.org/publication/KrebbersLW14},
  cites = {0},
  citedby = {0},
  pages = {543-548},
  booktitle = {itp},
}

@article{Leroy00,
  title = {A modular module system},
  author = {Xavier Leroy},
  year = {2000},
  researchr = {https://researchr.org/publication/Leroy00},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {10},
  number = {3},
  pages = {269-303},
}

@inproceedings{Leroy16,
  title = {Formally Verifying a Compiler: What Does It Mean, Exactly?},
  author = {Xavier Leroy},
  year = {2016},
  doi = {10.4230/LIPIcs.ICALP.2016.2},
  url = {http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.2},
  researchr = {https://researchr.org/publication/Leroy16},
  cites = {0},
  citedby = {0},
  booktitle = {icalp},
}

@inproceedings{PessauxL99,
  title = {Type-Based Analysis of Uncaught Exceptions},
  author = {François Pessaux and Xavier Leroy},
  year = {1999},
  doi = {10.1145/292540.292565},
  url = {http://doi.acm.org/10.1145/292540.292565},
  tags = {rule-based, exceptions, analysis},
  researchr = {https://researchr.org/publication/PessauxL99},
  cites = {0},
  citedby = {0},
  pages = {276-290},
  booktitle = {POPL},
}

@inproceedings{HirschowitzL02,
  title = {Mixin Modules in a Call-by-Value Setting},
  author = {Tom Hirschowitz and Xavier Leroy},
  year = {2002},
  url = {http://link.springer.de/link/service/series/0558/bibs/2305/23050006.htm},
  researchr = {https://researchr.org/publication/HirschowitzL02},
  cites = {0},
  citedby = {0},
  pages = {6-20},
  booktitle = {ESOP},
}
@proceedings{tic:1998,
  title = {Types in Compilation, Second International Workshop, TIC  98, Kyoto, Japan, March 25-27, 1998, Proceedings},
  year = {1998},
  researchr = {https://researchr.org/publication/tic%3A1998},
  cites = {0},
  citedby = {0},
  booktitle = {Types in Compilation, Second International Workshop, TIC  98, Kyoto, Japan, March 25-27, 1998, Proceedings},
  editor = {Xavier Leroy and Atsushi Ohori},
  volume = {1473},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-64925-5},
}

@proceedings{popl:2004,
  title = {Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004},
  year = {2004},
  tags = {programming languages, principles, programming},
  researchr = {https://researchr.org/publication/popl%3A2004},
  cites = {0},
  citedby = {0},
  booktitle = {Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004},
  conference = {POPL},
  editor = {Neil D. Jones and Xavier Leroy},
  publisher = {ACM},
  isbn = {1-58113-729-X},
}

@proceedings{cpp-2015,
  title = {Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015},
  year = {2015},
  url = {http://dl.acm.org/citation.cfm?id=2676724},
  researchr = {https://researchr.org/publication/cpp-2015},
  cites = {0},
  citedby = {0},
  booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015},
  conference = {CPP},
  editor = {Xavier Leroy and Alwen Tiu},
  publisher = {ACM},
  isbn = {978-1-4503-3296-5},
}