Xavier Leroy appointed to the French Academy of Sciences: a life devoted to computing

A long-standing passion for computer science

In the eyes of many of his fellow researchers in mathematics and computer science, both in France and overseas, the career of Xavier Leroy has been nothing short of remarkable. The prestigious scientific prizes he has been awarded over the past decade are testament to his creativity as a computer scientist and his talents as a programmer, having made significant contributions to the development of formal methods and functional languages.

Xavier Leroy has also excelled through his unwavering commitment to developing computer science and representing it beyond its inner circle. This impressive researcher has just earned further recognition, with his recent appointment to the French Academy of Sciences.

Pivotal meetings with fellow scientists

The people Xavier Leroy has met along his journey to becoming a visionary computer scientist have been hugely important.  This dates back to the mid-1980s when, still at secondary school, he paid a visit to a theoretical physics laboratory at the University of Orléans. He has fond memories of this first encounter with scientists; as a teenager, he already had a keen interest in science and computing, which he had discovered the fundamentals of while tinkering with a PC, like many young people at the time.

It was at the École Normale Supérieure, where he enrolled in 1987, that Xavier Leroy made his first forays into computing: “Mathematics at the ENS was the pinnacle, but I struggled with it, and I switched to IT. I found the scope and scientific discipline of algorithmics, computer algebra and programming just as appealing as mathematics”, recalls the researcher.

His career began with a first-year internship at Inria exploring the functional programming language Caml, supervised by Guy Cousineau:

The institute was already very much at the forefront from a digital perspective, with cutting-edge equipment and pioneering researchers in those disciplines.

Dedication to research

After his Master’s studies, Xavier Leroy began a PhD in computer science under the supervision of Gérard Huet, a major name in the field. Upon completing his PhD in 1993, he joined the University of Stanford for a two-year postdoctoral placement: 

I was fortunate enough to meet computing pioneers, at the heart of Silicon Valley, on a campus with extraordinary resources. That was an unforgettable experience. When I got back to France, it was clear that Inria was the right place to carry out my research.

Leroy joined Inria in 1994 as a research fellow, where he developed and perfected Caml, a language that would go on to become OCaml. One of Inria’s flagship achievements, OCaml has been used to develop a range of software programs used in both research - including the Coq proof assistant, a trusted ally for mathematical reasoning - and industry. “I spent several years fine-tuning OCaml. Distributed in its 5.0 version in 2022, it is accessible open source and can be used to develop applications with very high guarantees in terms of safety and reliability. After being used in industry (aeronautics, space and nuclear), we are now seeing it being used for applications linked to systems, the blockchain and financial computing.”

A wealth of experience in research and teaching

In the late 1990s, Xavier Leroy developed an interest in computer security and spent a number of years with the startup Trusted Logic, a specialist in this field. Working alongside its founder Dominique Bolignano, his job was as scientific advisor: “I was 32 at the time, making me one of the older members of a team where dynamism and creativity were a prerequisite.” 

After returning to Inria following the sale of Trusted Logic in 2002, Xavier Leroy worked with Sandrine Blazy on the design and formal verification of CompCert, a compiler for C language. Over time, the reliability of this compiler, which has been demonstrated mathematically, has seen it come to be used in both academia and industry - particularly for the development of critical programs in sensitive industries such as aeronautics and nuclear.

These major projects were unanimously praised by his peers, and Xavier Leroy won a number of awards prior to being made a professor at the Collège de France in 2018, where he holds a permanent chair in “Software Science”, just like his illustrious predecessor Gérard Berry. “It’s an enormous honour to get to represent computer science within one of the oldest institutions in France. The Collège de France is also highly innovative, offering all its courses online, including the traditional introductory lecture. Passing on knowledge to as many people as possible is hugely rewarding, but it's also a lot of work as you have to keep coming up with original courses each year.”

Recognition for an exemplary career

Splitting his time between teaching at the Collège de France and research at Inria (where he is still a member of Cambium) Xavier Leroy was surprised to find he was being appointed to the French Academy of Sciences. 

I wasn't expecting it. It’s obviously a big honour, but my main feeling is pride at getting to represent IT, following on from the first generation of French IT pioneers such as Gérard Huet, Gérard Berry and Serge Abiteboul. Computer science has now been recognised as a scientific discipline in its own right, and that makes me really happy.

Xavier Leroy hopes to be able to use this appointment to become an ambassador for computer science and raise awareness of the originality of his discipline. Computing is technology that has become part of everyday life for companies and people, and has been used to develop whole sections of our economy. But it’s also a science rooted in fundamental knowledge in areas such as programming, languages and data, drawing on rigorous concepts and constantly evolving.

Far from signifying the end of his career, this appointment to the French Academy of Sciences marks the beginning of a new era for Xavier Leroy:

I plan to continue to explore open questions in CS and to promote it as a discipline. The scientific dimension to CS, which isn’t as familiar to the wider public or decision-makers in the worlds of business and politics, is essential to its progress. Without theoretical research in CS, future innovations that will benefit everyone won't be possible.

• Cambium unveils a new version of OCaml programming language, Inria, 16/12/2022.
• CompCert software program receives a prestigious award, Inria, 29/6/2022.
• Software: between mind and matter, introductory lecture by Xavier Leroy (video), Collège de France, 15/11/2018.
• Xavier Leroy: Inria - French Academy of Sciences Grand Prize, Inria, 29/10/2018.
• With Xavier Leroy, computer science confirms its presence at the Collège de France, Inria, 15/6/2018.
• Why create new programming languages? Interstices, 28/01/2019.