Yves Bertot (Research and teaching)

Research team, Recent publications, All publications, talks, Teaching, Formal proofs, Algorithms, Collaborations, binaries, Popularization (in French), Internships, My blog on Coq, More personnal stuff.

Formalizing mathematics and algorithms

My main research interest revolves around the formal description of algorithms and mathematical theories. By formal description, I mean descriptions that can be completely checked by computer programs: theorem proving tools.

We talk about theorem proving tools, because we try to prove every property that we state about algorithms. So each new algorithm that we study gives rise to a few theorems that need to be entirely verified on the computer. At least one theorem has the statement of the form, if we feed this algorithm inputs that satisfy property so and so, then the algorithm performs without error and returns outputs that satisfy such and such properties.

the long term dream is that this kind of technique could be used to develop all the software that we use in everyday life, so that bugs would be detected very early in the design process. A bug would appear when some algorithm requires that its input has a given property, but this algorithm receives its outputs from another algorithm which only ensures a weaker property. Checking that some property entails another one is also among the theorems that we need to prove.

The current research work is to understand why this kind of technique cannot be applied today and fill in the gaps. As far as I know, there are the following problems:

1. Software developers don't even know that these techniques exist and are useful,
2. There are algorithms that one can program but one cannot formalize,
3. What we can say about algorithms is not what we want to say.

Distinctions

I received the 2013 Software System Award as one of the main contributors for the Coq system, along Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chet. Murthy, and Pierre Castéran (see the video from ACM and the picture from the ceremony).

Multimedia material

I prepared a multi-media course providing an introduction to the Coq system. This course is in French and was available here available here, but this link is only available from within Inria since 2017. A downgraded version is available here

Schools and intensive courses

In 2023, I taught a course on Coq for mathematics a school entitled "Interactions of Proof Assistants and Mathematics" organized in Regensburg, Germany. My specific course material is available here.

Since 2007, I have taught at a variety of schools, mainly around the semantics of programming languages and the usage of Coq. While I often had an influence on the school's programs, the organization was most of the time take care of by others. The next schools are Cea-Edf-Inria school on Modelling and verifying algorithms in Coq to be held in November 2011 at INRIA Paris, and Spring School on Formalization of Mathematics to be held in March 2012 at INRIA Sophia Antipolis.

In reverse chronologic order, the previous schools are 3rd Asian-Pacific Summer School on Formal Methods, 2nd Asian-Pacific, 1st Asian-Pacific, 2008 Tsinghua, Beijing School on Coq, Lernet summer school, Semantics of Programming Languages in Calculus of Constructions, Chalmers.

Events

I am proud to have participated in the the math-components project, as part of the Microsoft-Inria Joint Centre, especially for the achievement on the formal proof of the Feit-Thompson theorem.

Recent publications

Yves Bertot Safe Smooth Paths Between Straight Line Obstacles Logics and Type Systems in Theory and Practice, LNCS 14560, Springer, 2024. (preprint)

Andrew Appel, Yves Bertot C floating-point proofs layered with VST and Flocq Journal of Formalized Reasoning, December 2020