Xavier Leroy

Q: What Schools Are Affiliated With Xavier Leroy

Xavier Leroy is affiliated with the following schools: Paris Sciences et Lettres University, Paris Diderot University

Xavier Leroy's AcademicInfluence.com Rankings

Xavier Leroy

Computer Science

#390

World Rank

#406

Historical Rank

Database

#4893

World Rank

#5082

Historical Rank

computer-science Degrees

Download Badge

Computer Science

Why Is Xavier Leroy Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Xavier Leroy is a French computer scientist and programmer. He is best known for his role as a primary developer of the OCaml system. He is Professor of software science at Collège de France. Before his appointment at Collège de France in 2018, he was senior scientist at the French government research institution Inria.

(See a Problem?)

Xavier Leroy's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

Formal verification of a realistic compiler (2009) (1190)
Formal certification of a compiler back-end or: programming a compiler with a proof assistant (2006) (763)
A Formally Verified Compiler Back-end (2009) (510)
Manifest types, modules, and separate compilation (1994) (311)
The Objective Caml system release 3.09 Documentation and user''s manual (2005) (241)
Unboxed objects and polymorphic typing (1992) (241)
A concurrent, generational garbage collector for a multithreaded implementation of ML (1993) (235)
The ZINC experiment : an economical implementation of the ML language (1990) (220)
Coinductive big-step operational semantics (2006) (214)
A compiled implementation of strong reduction (2002) (207)
The Objective Caml system release 2.04 (2002) (188)
Mechanized Semantics for the Clight Subset of the C Language (2009) (187)
Java Bytecode Verification: Algorithms and Formalizations (2003) (185)
Formal Verification of a C Compiler Front-End (2006) (169)
Applicative functors and fully transparent higher-order modules (1995) (167)
Managing the Complexity of Large Free and Open Source Package-Based Software Distributions (2006) (165)
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations (2008) (159)
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection (2003) (140)
Type-based analysis of uncaught exceptions (2000) (137)
A Formally-Verified C Static Analyzer (2015) (132)
The OCaml system release 4.07: Documentation and user's manual (2013) (131)
A modular module system (2000) (127)
Dynamics in ML (1991) (123)
Bytecode verification on Java smart cards (2002) (120)
Formal verification of translation validators: a case study on instruction scheduling optimizations (2008) (103)
Polymorphic type inference and assignment (1991) (96)
Java Bytecode Verification: An Overview (2001) (93)
Security properties of typed applets (1998) (92)
Validating LR(1) Parsers (2012) (90)
Abstract Types and the Dot Notation (1990) (82)
Benchmarking implementations of functional languages with ‘Pseudoknot’, a float-intensive benchmark (1996) (81)
Mixin modules in a call-by-value setting (2002) (79)
CompCert - A Formally Verified Optimizing Compiler (2016) (72)
The CompCert Memory Model, Version 2 (2012) (70)
A syntactic theory of type generativity and sharing (1996) (69)
Polymorphism by name for references and continuations (1993) (68)
Polymorphic typing of an algorithmic language (1992) (63)
A simple, verified validator for software pipelining (2010) (63)
A formally verified compiler for Lustre (2017) (60)
Verified validation of lazy code motion (2009) (60)
Formal certification of a compiler back - end (2005) (51)
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic (2013) (50)
On-Card Bytecode Verification for Java Card (2001) (49)
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis (2004) (48)
The effectiveness of type-based unboxing (1997) (47)
The CompCert C verified compiler (2015) (46)
Verified Compilation of Floating-Point Computations (2015) (38)
Types in Compilation (1998) (38)
Parallel Functional Programming with Skeletons: the OCamlP3L experiment (1998) (38)
Formal C Semantics: CompCert and the C Standard (2014) (38)
The CompCert C verified compiler: Documentation and user’s manual (2015) (37)
Compilation of extended recursion in call-by-value functional languages (2003) (35)
Mechanized Verification of CPS Transformations (2007) (35)
A Formally-Verified Alias Analysis (2012) (35)
Validating Register Allocation and Spilling (2010) (35)
CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler (2018) (33)
Formal Verification of a Memory Model for C-Like Imperative Languages (2005) (31)
Formally verified optimizing compilation in ACG-based flight control software (2012) (31)
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves (2008) (27)
Le système Caml Special Light: modules et compilation efficace en Caml (1995) (27)
Pseudoknot: A Float-Intensive Benchmark for Functional Compilers (1994) (26)
A locally nameless solution to the POPLmark challenge (2007) (26)
Towards Formally Verified Optimizing Compilation in Flight Control Software (2011) (25)
Maintaining large software distributions: new challenges from the FOSS era. (2006) (25)
Formal verification of object layout for c++ multiple inheritance (2011) (25)
Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types (2004) (21)
Documentation and user''''s manual (2004) (21)
A proposal for recursive modules in Objective Caml (2003) (20)
Closing the Gap – The Formally Verified Optimizing Compiler CompCert (2017) (19)
A Bytecode-Compiled, Type-safe, Multi-Stage Language (2001) (18)
EDOS: Environment for the Development and Distribution of Open Source Software (2005) (18)
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004 (2004) (18)
A mechanized semantics for C++ object construction and destruction, with applications to resource management (2012) (17)
The CompCert memory model (2014) (17)
Mechanized Semantics for Compiler Verification (2012) (16)
Efficient Data Representation in Polymorphic Languages (1990) (16)
Principles and a Preliminary Design for ML2000 (2000) (14)
Type-based analysis of uncaught exceptions (1999) (14)
A List-Machine Benchmark for Mechanized Metatheory (2012) (14)
Mechanized semantics - with applications to program proof and compiler verification (2010) (13)
A verified framework for higher-order uncurrying optimizations (2009) (12)
Verified squared: does critical software deserve verified tools? (2011) (11)
Embedded Program Annotations for WCET Analysis (2018) (9)
Computer Security from a Programming Language and Static Analysis Perspective (2003) (9)
A reduction semantics for call-by-value mixin modules (2002) (9)
Verified code generation for the polyhedral model (2021) (7)
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract) (2007) (7)
Program Logics for Certified Compilers: Hoare logic (2014) (6)
Mechanized semantics (2010) (6)
Formal verification of an optimizing compiler (2007) (6)
An overview of Types in Compilation (1998) (5)
News from the EDOS project: improving the maintenance of free software distributions. (2006) (5)
On the implementation of recursion in call-by-value functional languages (2003) (4)
On-ard Byte ode Veri ation for Java Card (2001) (4)
New Results - Implémentations de Caml (2002) (3)
Keynote II: Formally verifying a compiler: Why? How? How far? (2011) (3)
Compiler verification for fun and profit (2014) (3)
Programmation du systeme Unix en Caml Light (1993) (3)
Proceedings of the 2005 ACM SIGPLAN Workshop on ML (2006) (2)
Safety first! (2011) (2)
Compilation of extended recursion in call-by-value functional languages (2009) (2)
Formal Proofs of Code Generation and Verification Tools (2014) (2)
How I found a crash bug with hyperthreading in Intel's Skylake processors (2017) (2)
Formally Verifying a Compiler: What Does It Mean, Exactly? (2016) (2)
Higher order separation logic (2014) (1)
Program Logics for Certified Compilers: Mechanized Semantic Library (2014) (1)
Proceedings of the Second International Workshop on Types in Compilation (1998) (1)
Formal verification of a static analyzer: abstract interpretation in type theory (2014) (1)
In Search of Software Perfection (2019) (1)
New Results - The Objective Caml system, tools, and extensions (2007) (1)
OcamlP 3 l 2 . 0 : User Manual (2007) (1)
Towards Optimizing Certified Compilation in Flight Control Software ∗ (2010) (1)
Software, between mind and matter (2020) (0)
Contracts and Grants with Industry - The Caml Consortium (2011) (0)
From separation algebras to separation logic (2014) (0)
Higher-order Hoare logic (2014) (0)
KER volume 27 issue 2 Cover and Back matter (2012) (0)
Program Logics for Certified Compilers: Covariant recursive predicates (2014) (0)
Modeling the Hoare judgment (2014) (0)
New Results - The OCaml language and system (2015) (0)
2 Contents (2022) (0)
More C programs (2014) (0)
New Results - The Objective Caml system, libraries and tools (2003) (0)
Heap theorem prover (2014) (0)
New Results - Formal verification of compilers (2007) (0)
Flow Caml in a Nutshell (2003) (0)
Partnerships and Cooperations - Regional initiatives (2011) (0)
Program Logics for Certified Compilers: Share accounting (2014) (0)
Dissemination - Animation de la communauté scientifique (2002) (0)
Programming languages, types, compilation and proofs (2006) (0)
Case study: Lambda-calculus with references (2014) (0)
MPRI course 2-4 “ Functional programming languages ” Answers to the exercises (2007) (0)
Introduction to step-indexing (2014) (0)
Program Logics for Certified Compilers: The VST separation logic for C light (2014) (0)
Program Logics for Certified Compilers: Separation logic (2014) (0)
New Software and Platforms - CompCert C (2014) (0)
Program Logics for Certified Compilers: Simplification by rewriting (2014) (0)
[Solitary calcified myofibroma of the leg: a case report]. (2011) (0)
Synthèse – conclusion: Synthesis – conclusion (2013) (0)
Formal Verification of Code Generators for Modeling Languages: Invited Presentation at the Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (2018) (0)
Carcinomes rénaux à translocation: Translocation associated renal cell carcinoma (2013) (0)
Special Issue Dedicated to ICFP 2009 Editorial (2011) (0)
Semantic model and soundness of Verifiable C (2014) (0)
Program Logics for Certified Compilers: Introduction (2014) (0)
Proceedings of the 2015 Conference on Certified Programs and Proofs (2015) (0)
Program integrity of Control Method for verification of execution traces of footprints (2003) (0)
Program Logics for Certified Compilers: Proof of a program (2014) (0)
Program Logics for Certified Compilers: Bibliography (2014) (0)
Program Logics for Certified Compilers: Separation algebras (2014) (0)
Separation logic for CompCert (2014) (0)
Expressions, values, and assertions (2014) (0)
Data structures in indirection theory (2014) (0)
Preface (2005) (0)
Derived rules and proof automation for C light (2014) (0)
Control of access to data by dynamic verification of legal references (2003) (0)
A Bytecode-Compiled , Type-saf e , Multi-Sta ge Langua ge Cristiano Calcagno (2001) (0)
THE VERIFIERS ? łCan you trust your compiler ? ž So began (2019) (0)
Predicate implication and subtyping (2014) (0)
How to specify a compiler (2014) (0)
Applying higher-order separation logic (2014) (0)
Separation algebra for CompCert (2014) (0)
ROB volume 31 issue 1 Cover and Back matter (2012) (0)
Foundational static analysis (2014) (0)
A propos du centre ou de la direction fonctionnelle (2017) (0)
Typechecking for Verifiable C (2014) (0)
New Results - The Objective Caml system and extensions (2008) (0)
C light operational semantics (2014) (0)
A Simple, Verified Validator for Software Pipelining (verification pearl) (2010) (0)
New Results - Mechanization of type systems and axiomatic and operational semantics (2007) (0)
New Results - Formal management of software dependencies (2006) (0)
Semantic models of predicates-in-the-heap (2014) (0)
Higher-order semantic models (2014) (0)
Operational semantics of CompCert (2014) (0)
Lifted separation logics (2014) (0)
Soundness of Hoare logic (2014) (0)
Histoséminaire sur le cancer de prostate : nouveautés OMS 2016 — cas no 04 : adénocarcinome prostatique mucineux Prostate cancer histoseminar : Update of the 2016 WHO classification — case no 4 : Mucinous prostatic adenocarcinoma (2017) (0)
Inaugural lecture at Collège de France Software, between mind and matter (2019) (0)
Program Logics for Certified Compilers: Generic separation logic (2014) (0)
First-order separation logic (2014) (0)
Industrial uses of Caml: examples and lessons learned from the smart card industry (2007) (0)
General recursive predicates (2014) (0)
unix system programming in objective caml (2010) (0)
Program Logics for Certified Compilers: Road map (2014) (0)
Objects, classes and modules in Objective Caml (invited lecture, abstract only) (1999) (0)
Types in Compilation: Second International Workshop, TIC'98, Kyoto, Japan, March 25-27, 1998 Proceedings (1998) (0)
A Structured Approach to Defence Simulation Training Reverie – Real and Virtual Come Together in a Virtual Reality the D-cent Project: Decentralized Social Software for Political Autonomy 9 Bluebridge -new Data Services for an Ecosystem Approach to Fisheries (2015) (0)
New Results - Compilation certifiée de la réduction forte (2002) (0)
Type-based analysis of un aught ex eptions XAVIER LEROY and FRANC OIS PESSAUX (2014) (0)
Session details: Verification (2010) (0)
Modular structure of the development (2014) (0)
Semantic model of CSL (2014) (0)
Concurrent separation logic (2014) (0)
New Software and Platforms - OCaml (2015) (0)
Operators on separation algebras (2014) (0)
A little case study (2014) (0)
New Results - Formal verification of compilers and static analyzers (2011) (0)
Program Logics for Certified Compilers: Separation logic as a logic (2014) (0)
Functional programming languages Part V: functional intermediate representations (2007) (0)
New Results - Applications de Caml (2002) (0)
Case study: Separation logic with first-class functions (2014) (0)
Dependently typed C programs (2014) (0)
CPC volume 21 issue 1-2 Cover and Back matter (2012) (0)

This paper list is powered by the following services:

Other Resources About Xavier Leroy

What Schools Are Affiliated With Xavier Leroy?

Xavier Leroy is affiliated with the following schools: