Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Xavier Leroy's home page
Disclaimer: this home page was designed in 1994. In those
days, a home page consisted of a picture in the top left
corner, followed by a vitae and a list of publications. I decided to
keep it this way as a souvenir of the early days of the Web.
Some amusing (to me, at least) material can be found here if one
looks hard enough...
I'm interested in most aspects of computer programming, in particular
in programming languages, tools, and systems to make programs safer,
easier to write, and more efficient.
Most of my work deals with type systems, module systems and static analyses
to detect statically large classes of programming errors, ensure
safety properties in programs, and support software reuse and
parameterization in type-safe ways.
I also have a long-standing fascination for compilers, and have worked
quite a lot on the efficient compilation of the ML language, resulting in
the Objective Caml system.
These days, I'm having great fun trying to prove semantic preservation for
lightly-optimizing compilers using the Coq proof assistant.
I'm also a firm believer in formal methods, and have a general
interest in formal semantics of programming languages (in particular
operational semantics) and machine-assisted proofs.
I am the proud architect and main developer of the Objective Caml system, an implementation of the
Caml dialect of ML that supports equally well functional, imperative
and object-oriented programming, all brought together by an ML-style
static type system with polymorphism and type inference.
Objective Caml's object system, due to Didier Rémy
and Jérôme Vouillon, is the first to offer
ML-style type inference within a full class-based OO language.
Other noticeable features include a powerful SML-style module calculus,
a bytecode compiler that generates portable intermediate code that
runs very efficiently, and a native-code compiler that generates
high-performance assembly code for a variety of platforms.
Various Caml libraries and tools that I developed as side projects
are collected in this page.
I'm also a happy user of Linux. My contribution to the Linux effort is
LinuxThreads, a thread
library for Linux implementing the Posix 1003.1c standard for threads.
In parallel, I have also worked on smart cards, more specifically on
compact, efficient and secure Java execution environments for Java Card
(Java-enabled smartcards), first as a consultant for Bull CP8, then at Trusted Logic.
I am involved in the MPRI, a
research-oriented graduate curriculum in computer science,
co-organized by several Parisian universities and grandes écoles.
If you are interested in doing a PhD in my group, here is some information
on doing a PhD at INRIA.