Abstract
Xavier Leroy's research focuses on new programming languages and tools, and on the formal verification of mission-critical software to guarantee its safety and security. He is the architect and one of the main developers of the OCaml functional programming language and the CompCert formally verified C compiler, two major software products resulting from his research.
Functional languages, type systems and practical applications : the Caml Light and OCaml languages
Xavier Leroy trained in mathematics and computer science at the École normale supérieure, then at INRIA, where he completed his thesis. A prodigious programmer, he distinguished himself through a series of leading works on type systems and module systems for functional languages, which led to the development of Caml Light, now OCaml, one of the two most widely used typed functional languages in the world, in fields as diverse as aeronautics, finance and the Web. This language is used to develop a wide range of software tools, such as the Coq proof assistant, the Astrée and Frama-C static analyzers, the SCADE 6 compiler from Estérel Technologies and the Tezos blockchain. OCaml has been used in many emblematic projects, such as the web version of Facebook Messenger, the MediaWiki software and the Docker virtualization infrastructure.
Program proof, compiler proof and practical application : the CompCert compiler
Xavier Leroy is also behind CompCert, a certified C compiler written and verified using the Coq proof assistant. This is a world first in several respects : it allows formal verification of unprecedented size and complexity, and above all, it offers the possibility of having a certified compiler, a key step in the certification and automatic verification of software chains, and therefore towards " zero defect " programming. This feat of arms has had a considerable impact on the very nature of major software research programs.
Appointed Professor at the Collège de France, Xavier Leroy will occupy the Software Science chair, where he will be teaching a series of lectures from the 2018-2019 academic year entitled Programmer = demonstrate ? Curry-Howard correspondence today.
