Xavier Leroy : Inria - French Académie des sciences Grand Prize
Date:
Publish on 17/01/2020
In November 2018, Xavier Leroy will join the Collège de France as the ‘Software Sciences’ chair. A marvellous acknowledgement for the architect of two great Inria successes: the functional programming language OCaml and the formally verified compiler CompCert.
Like many, it was in his teenage bedroom that Xavier Leroy became acquainted with computing. “Back then, it was the beginning of personal computers and their capacities were limited to say the least... But I do remember trying to write small programs. It was fun, but above all frustrating!” He didn’t fall in love until later, during his first year at the École Normale Supérieure (ENS) in Paris, with the discovery of fundamental computing, an exciting universe of great formal purity. After completing an internship in Silicon Valley, he became a member of the joint ENS and Inria Rocquencourt team Formel for a PhD on type systems for the ML language family, before returning to the United States, this time to Stanford, for a post-doc.
From CAML to Caml Light to OCaml
“In 1994, I joined Inria for good, having been recruited by the Cristal project team, still in Rocquencourt, to continue my research on functional programming languages. ” This work had begun with a limited but effective implementation of the Caml language, called Caml Light, which led to the language spreading, especially in France, for teaching programming. “Gradually, it grew in stature and evolved into a very complete language called OCaml, now used in research as well as in industry (finance, security, Web services, etc.) ”
On track for zero errors
At the end of the 1990s, Xavier Leroy broadened his horizons and took a greater interest in the role that programming languages can have in IT security. These questions led to him contributing to the creation of a start-up specialised in the security of smart cards (Trusted Logic) – a collaboration that would last five years. “In 2004, I returned to Inria full time and, drawing on what I learned at Trusted Logic, I dived into the world of formal methods with the verification of critical software in my sights, such as that used in smart cards as well as in electronic aircraft controls, driverless metros and nuclear power plant control systems. ” At the head of his team – which became Gallium in 2006 – Xavier Leroy then focused his research on the formal verification of compilers, the programs responsible for translating source code written in a high-level programming language into machine language and which, as such, are essential components in the critical software security chain. Because, in the same way as a misinterpretation in a translation between natural languages changes the meaning of a text, a bug in a compiler can cause it to produce machine code that does not respect the intentions expressed in the source program.
CompCert: a milestone in the formal verification of compilers
“That's how we created CompCert, a compiler for the C language commonly used for critical software. Its strong point: it ensures that each compilation pass is backed up by a mathematical proof that guarantees that the semantics of the program are preserved. To do this, it uses the proof assistant Coq, which was developed by Inria. ” In 2011, a randomised test study compared CompCert and the other main C compilers. And while hundreds of bugs were identified for its competitors, CompCert’s results were faultless! It is not surprising that the made-in-Inria tool has met with great academic interest and revitalised research into the formal verification of compilers. “In industry, interest is also growing. A few years ago we signed a marketing partnership with Absint, a German SME, and today we have our first industry user in the form of MTU, a company that manufactures components for the nuclear industry, with Airbus also closely studying the possibility of using CompCert for some of its embedded software. ”
New start, new fields of research
Very proud of the success of OCaml and CompCert, Xavier Leroy is now entering a new phase of his life, with an appointment to the Collège de France as the permanent ‘Software Sciences’ chair. Coincidentally, this Inria – Académie des Sciences Grand Prize comes at a time when Xavier Leroy is about to distance himself from an institute where he will have spent the bulk of his life as a researcher. “I owe a lot to Inria, which has supported our work over time, without demanding a return in the short term. I want to see this award as a sign that there is still room for long-term research in fundamental computer science at Inria! ” But these teaching activities will not prevent Xavier Leroy from pursuing his research. “As I was preparing my inaugural lecture, I realised that I wanted to reconnect with other areas of research ,” he concludes. “I would now like to explore new subjects, such as languages to better program massively parallel hardware, or even the development of formal verification in the age of deep learning: how will we verify software that is no longer entirely written but partially learned? But I also want to take the time to take an interest in ethical issues, in particular the threats that digital technology could pose to individual freedoms and democratic processes. It is a subject that concerns me not only as a scientist, but also as a citizen! ”
Bio express
Born in 1968, Xavier Leroy studied mathematics and then computer science at the École Normale Supérieure (ENS) in Paris. Following a PhD in fundamental computer science from Paris 7 University, he then went to the United States as a post-doctoral researcher at the University of Stanford (California). Upon his return to France, he joined Inria in 1994. At the end of the 1990s, he contributed to the creation of the start-up Trusted Logic, specialising in IT security. In 2004, he became leader of the Cristal project team, then, in 2006, of the Gallium project team, specialised in programming languages and systems. In May 2018, he was appointed professor at the Collège de France.