With Xavier Leroy, computer science confirms its presence at the Collège de France

What have your main research areas been at Inria? 

With the Gallium team created in 2006 - and even previously with the Cristal team - I have focused on what can make software more reliable or of better quality. First of all our approach focused on programming languages, to make them more expressive, more secure and simpler. One of our visible results is the OCaml programming language, which was quite successful.

When Gallium was created, we wanted to extend our scope by working on the proof of programs - i.e. the way in which the reliability of software can be mathematically proven - and, more specifically, compilers. Moreover, in our work we use technologies originating from Inria such as the Coqproof assistant. This led to the Compcertproject, the first realistic compiler to have been mathematically verified.

What does this appointment to the Collège de France represent for you?

It is a great honour for me to be appointed to such an institution. However, it is also about recognition for the discipline. Indeed, it has taken computer science some time to be recognised by the French university system - 20 to 30 years after the United States or the United Kingdom.

It was Gérard Berry - also from Inria - who brought computer science to the Collège de France, firstly with two annual chairs in 2007 and 2009, then with the "Algorithms, Machines and Languages" permanent chair from 2012. I am very pleased to be following the path carved out by Gérard, who will soon be retiring. An admirable teacher, through sharing his enthusiasm and knowledge he has made himself the ambassador of computer science.

Moreover, I see the creation last year of Stéphane Mallat's "Data Sciences" chair as another very good sign for the discipline. Our two teaching areas could be very complementary in their approach to the problems of modern computer science.

What type of content do you wish to teach? 

I will try to explain the founding principles of the software sciences. In other words, what are the mathematical principles that make it possible to reason out, build and verify software, languages or programming tools. I want to show the mathematical precision that can be injected into all software-based activities.

Subsequently, I would like to present the history of the concepts in order to enable an understanding of how some have emerged, but also - and above all - to report on contemporary research, science "that is in the making". For example, by presenting certain advances that have taken place over the last ten years that enable ideas that are first of all fundamental to now become usable by industry. Or everything that revolves around machine learning. This is a complete game-changer. Certain software programs today are no longer truly written, but instead learned using examples. How then do we reason out on this or ensure their reliability? I would like to open up these lines of thought in my teaching.

And what about the style of your classes?

Teaching at the Collège de France is not like giving a Master's course. The lectures are open to everyone, both on-site and online, and the audience is very diverse, from the general public to researchers who are specialists in the field.

It is therefore not easy to find the ideal combination between the technical nature of the knowledge and its accessibility in order to be able to communicate a few simple instincts and attract new people to the discipline. Moreover, that is something I had the opportunity to discuss with all of the Collège de France professors during my candidacy. For me, it will be one of the challenges to address during the inaugural lecture planned for mid-November, then during my lectures which will continue until the end of January. 

BIOGRAPHY

Born in 1968, Xavier Leroy studied mathematics and then computer science at the graduate school É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 head of the Cristal team then, in 2006, of the Gallium team, specialised in programming languages and systems.