Skip to Main content Skip to Navigation

inria-00077018v1  Reports
Xavier Leroy. Polymorphic typing of an algorithmic language
[Research Report] RR-1778, INRIA. 1992
hal-01499983v1  Conference papers
Xavier Leroy. Efficient data representation in polymorphic languages
PLILP 1990: Programming Language Implementation and Logic Programming, Aug 1990, Linköping, Sweden. ⟨10.1007/BFb0024189⟩
tel-01499951v1  Theses
Xavier Leroy. Typage polymorphe d'un langage algorithmique
Langage de programmation [cs.PL]. Université Paris 7, 1992. Français
inria-00073825v1  Reports
Xavier Leroy. A Modular Module System
[Research Report] RR-2866, INRIA. 1996
hal-01499972v1  Journal articles
Xavier LeroyMichel Mauny. Dynamics in ML
Journal of Functional Programming, Cambridge University Press (CUP), 1993, 3 (4), pp.431-463. ⟨10.1017/S0956796800000848⟩
hal-01499962v1  Conference papers
Marco DaneluttoRoberto Di CosmoXavier LeroySusanna Pelagatti. Parallel Functional Programming with Skeletons: the OCamlP3L experiment
ACM Workshop on ML and its applications, ACM, Sep 1998, Baltimore, United States
hal-01499966v1  Conference papers
Xavier Leroy. Applicative functors and fully transparent higher-order modules
POPL 1995: 22nd symposium Principles of Programming Languages, ACM, Jan 1995, San Francisco, United States. pp.142 - 153, ⟨10.1145/199448.199476⟩
hal-01499956v1  Conference papers
Xavier Leroy. On-card Bytecode Verification for Java Card
Smart card programming and security, proceedings E-Smart 2001, Sep 2001, Cannes, France. pp.150-164, ⟨10.1007/3-540-45418-7_13⟩
hal-01499955v1  Conference papers
Xavier Leroy. Java bytecode verification: an overview
Computer Aided Verification, CAV 2001, Jul 2001, Paris, France. pp.265-285, ⟨10.1007/3-540-44585-4_26⟩
hal-03000244v1  Journal articles
Nathanaël CourantXavier Leroy. Verified Code Generation for the Polyhedral Model
Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), pp.40:1-40:24. ⟨10.1145/3434321⟩
hal-01499957v1  Book sections
Xavier LeroyFrançois Rouaix. Security properties of typed applets
Jan Vitek; Christian D. Jensen Secure Internet Programming - Security issues for Mobile and Distributed Objects, 1603, Springer, pp.147-182, 1999, LNCS, 978-3-540-66130-6. ⟨10.1007/3-540-48749-2_7⟩
hal-01499938v1  Conference papers
Xavier Leroy. Computer Security from a Programming Language and Static Analysis Perspective
ESOP 2003: Programming Languages and Systems, 12th European Symposium on Programming, Apr 2003, Warsaw, Poland. pp.1 - 9, ⟨10.1007/3-540-36575-3_1⟩
inria-00289543v1  Conference papers
Andrew W. AppelXavier Leroy. A list-machine benchmark for mechanized metatheory (extended abstract)
Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. pp.95-108, ⟨10.1016/j.entcs.2007.01.020⟩
hal-01499964v1  Conference papers
Xavier Leroy. The effectiveness of type-based unboxing
TIC 1997: Workshop Types in Compilation, Jun 1997, Amsterdam, Netherlands
hal-01499939v1  Journal articles
Xavier Leroy. Java bytecode verification: algorithms and formalizations
Journal of Automated Reasoning, Springer Verlag, 2003, 30 (3-4), pp.235--269. ⟨10.1023/A:1025055424017⟩
hal-01499963v1  Conference papers
Xavier LeroyFrançois Rouaix. Security properties of typed applets
POPL 1998: 25th symposium Principles of Programming Languages, Jan 1998, San Diego, United States. pp.391-403, ⟨10.1145/268946.268979⟩
hal-01848686v1  Conference papers
Bernhard SchommerChristoph CullmannGernot GebhardXavier LeroyMichael Schmidt et al.  Embedded Program Annotations for WCET Analysis
WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, Jul 2018, Barcelona, Spain. ⟨10.4230/OASIcs.WCET.2018.8⟩
hal-01350287v1  Journal articles
Xavier Leroy. Comment faire confiance à un compilateur ?
Interstices, INRIA, 2010
hal-00359213v1  Journal articles
Tom HirschowitzXavier LeroyJ. B. Wells. Compilation of extended recursion in call-by-value functional languages
Higher-Order and Symbolic Computation, Springer Verlag, 2009, 22 (1), pp.3-66. ⟨10.1007/s10990-009-9042-z⟩
hal-00983850v1  Conference papers
Xavier Leroy. Proof assistants in computer science research
IHP thematic trimester on Semantics of proofs and certified mathematics, Institut Henri Poincaré, Apr 2014, Paris, France
inria-00289541v1  Conference papers
Zaynah DargayeXavier Leroy. Mechanized verification of CPS transformations
Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, Oct 2007, Erevan, Armenia. pp.211-225, ⟨10.1007/978-3-540-75560-9_17⟩
inria-00415861v1  Journal articles
Xavier Leroy. Formal verification of a realistic compiler
Communications of the ACM, Association for Computing Machinery, 2009, 52 (7), pp.107-115. ⟨10.1145/1538788.1538814⟩
inria-00123945v2  Reports
Xavier Leroy. A locally nameless solution to the POPLmark challenge
[Research Report] RR-6098, INRIA. 2007, pp.54
hal-00983847v1  Conference papers
Xavier Leroy. Formal verification of a static analyzer: abstract interpretation in type theory
Types - The 2014 Types Meeting, May 2014, Paris, France