Travelled to:1 × Austria
1 × Canada
1 × Cyprus
1 × Estonia
1 × Germany
1 × India
1 × Ireland
1 × Japan
1 × Poland
13 × USA
2 × Spain
2 × Sweden
5 × France
Collaborated with:∅ J.Tristan T.Hirschowitz T.Ramananandro G.D.Reis J.B.Wells J.Jourdan S.Blazy S.Rideau B.Grégoire F.Pessaux F.Rouaix D.Doligez M.Mauny P.Weis F.Pottier Z.Dargaye C.Calcagno W.Taha L.Huang V.Laporte D.Pichardie T.Bourke Lélio Brun P.Dagand M.Pouzet L.Rieg F.Mancinelli J.Boender R.D.Cosmo J.Vouillon B.Durak R.Treinen
Talks about:formal (9) compil (9) verifi (7) verif (6) type (6) valid (5) polymorph (4) languag (4) modul (4) implement (3)
Person: Xavier Leroy
DBLP: Leroy:Xavier
Facilitated 1 volumes:
EdContributed to:
2015
2014
20122012
20112011
20102010
20092008
2007
20062006
2006200620042003
2003
20032002
2002
2001199919981995199419931992
1991199119902017Wrote 34 papers:
- POPL-2015-JourdanLBLP #c
- A Formally-Verified C Static Analyzer (JHJ, VL, SB, XL, DP), pp. 247–259.
- SEFM-2014-Leroy #code generation #proving #tool support #verification
- Formal Proofs of Code Generation and Verification Tools (XL), pp. 1–4.
- ESOP-2012-JourdanPL #lr #parsing #validation
- Validating LR(1) Parsers (JHJ, FP, XL), pp. 397–416.
- POPL-2012-RamananandroRL #c++ #resource management #semantics
- A mechanized semantics for C++ object construction and destruction, with applications to resource management (TR, GDR, XL), pp. 521–532.
- CGO-2011-Leroy #compilation #how #question #verification #why
- Formally verifying a compiler: Why? How? How far? (XL).
- POPL-2011-Leroy #question #tool support
- Verified squared: does critical software deserve verified tools? (XL), pp. 1–2.
- POPL-2011-RamananandroRL #c++ #inheritance #layout #multi #verification
- Formal verification of object layout for c++ multiple inheritance (TR, GDR, XL), pp. 67–80.
- CC-2010-RideauL #validation
- Validating Register Allocation and Spilling (SR, XL), pp. 224–243.
- POPL-2010-TristanL #pipes and filters #validation
- A simple, verified validator for software pipelining (JBT, XL), pp. 83–92.
- PLDI-2009-TristanL #lazy evaluation #validation
- Verified validation of lazy code motion (JBT, XL), pp. 316–326.
- POPL-2008-TristanL #case study #optimisation #scheduling #validation #verification
- Formal verification of translation validators: a case study on instruction scheduling optimizations (JBT, XL), pp. 17–27.
- RTA-2007-Leroy #compilation #optimisation #verification
- Formal Verification of an Optimizing Compiler (XL), p. 1.
- ASE-2006-MancinelliBCVDLT #complexity #open source #scalability
- Managing the Complexity of Large Free and Open Source Package-Based Software Distributions (FM, JB, RDC, JV, BD, XL, RT), pp. 199–208.
- ESOP-2006-Leroy #induction #semantics
- Coinductive Big-Step Operational Semantics (XL), pp. 54–68.
- FM-2006-BlazyDL #c #compilation #verification
- Formal Verification of a C Compiler Front-End (SB, ZD, XL), pp. 460–475.
- POPL-2006-Leroy #certification #compilation #programming #proving
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant (XL), pp. 42–54.
- ESOP-2004-HirschowitzLW #call-by #mixin #reduction #semantics
- Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types (TH, XL, JBW), pp. 64–78.
- ESOP-2003-Leroy #perspective #programming language #security #static analysis
- Computer Security from a Programming Language and Static Analysis Perspective (XL), pp. 1–9.
- GPCE-2003-CalcagnoTHL #abstract syntax tree #implementation #multi #using
- Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection (CC, WT, LH, XL), pp. 57–76.
- PPDP-2003-HirschowitzLW #call-by #compilation #functional #recursion
- Compilation of extended recursion in call-by-value functional languages (TH, XL, JBW), pp. 160–171.
- ESOP-2002-HirschowitzL #call-by #mixin
- Mixin Modules in a Call-by-Value Setting (TH, XL), pp. 6–20.
- ICFP-2002-GregoireL #implementation #reduction
- A compiled implementation of strong reduction (BG, XL), pp. 235–246.
- CAV-2001-Leroy #bytecode #java #overview #perspective #verification
- Java Bytecode Verification: An Overview (XL), pp. 265–285.
- POPL-1999-PessauxL #analysis #exception #type system
- Type-Based Analysis of Uncaught Exceptions (FP, XL), pp. 276–290.
- POPL-1998-LeroyR #security
- Security Properties of Typed Applets (XL, FR), pp. 391–403.
- POPL-1995-Leroy #higher-order
- Applicative Functors and Fully Transparent Higher-Order Modules (XL), pp. 142–153.
- POPL-1994-Leroy #compilation
- Manifest Types, Modules, and Separate Compilation (XL), pp. 109–122.
- POPL-1993-DoligezL #concurrent #garbage collection #implementation #ml #parallel #thread
- A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML (DD, XL), pp. 113–123.
- POPL-1993-Leroy #continuation #morphism #polymorphism
- Polymorphism by Name for References and Continuations (XL), pp. 220–231.
- POPL-1992-Leroy #polymorphism #type system
- Unboxed Objects and Polymorphic Typing (XL), pp. 177–188.
- FPCA-1991-LeroyM #ml
- Dynamics in ML (XL, MM), pp. 406–426.
- POPL-1991-LeroyW #polymorphism #type inference
- Polymorphic Type Inference and Assignment (XL, PW), pp. 291–302.
- PLILP-1990-Leroy #data transformation #performance #polymorphism #representation
- Efficient Data Representation in Polymorphic Languages (XL), pp. 255–276.
- PLDI-2017-BourkeBDLPR #compilation
- A formally verified compiler for Lustre (TB, LB, PÉD, XL, MP, LR), pp. 586–601.