Research team,Recent publications, All publications, talks, Teaching, Formal proofs, Collaborations, binaries, Vulgarization (in French), Interships.

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:

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

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, Chet. Murthy, and Pierre Castéran (see the video from ACM and the picture from the ceremony).

I prepared a multi-media course providing an introduction to the Coq system. This course is in French and 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.

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.

**Yves Bertot**

Coq in a hurry, preprint, regularly updated (errata page).

**Georges Gonthier, Andrea Asperti, Jeremy Avigad, et al.**
__ A Machine-Checked Proof of the Odd Order
Theorem__
Proceedings of

**Yves Bertot, Frédérique Guilhot, Assia
Mahboubi**

**A formal study of Bernstein coefficients and
polynomials***Mathematical Structures in Computer Science* 21(4), pp 731-762,
2011. (DOI:10.1017/S0960129511000090)
Open archive preprint

**Jean-François Dufourd**, **Yves Bertot**

**Formal Study of Plane Delaunay Triangulation***Proceedings of Interactive Theorem Proving*, Springer Verlag, LNCS 6172,
pp. 211-226, 2010.
Open archive preprint

**Maxime Dénès, Benjamin Lesage, Yves Bertot, and Adrien
Richard**

__ Formal proof of theorems on genetic regulatory
networks__
In

**Yves Bertot**

__ Theorem-Proving Support in programming language semantics__,

**Yves Bertot, Vladimir Komendantsky**

**Fixed point semantics and partial recursion in coq
***PPDP '08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming* Valencia, Spain, 2008.
pages 89-96, Open archive
preprint, [bib]

**Yves Bertot**

__
Structural Abstract Interpretation: A Formal Study Using Coq__,

**Yves Bertot, Ekaterina Komendantskaya**

**Using Structural Recursion for Corecursion***Types 2008* S. Berardi, F Damiani, and U. de'Liguoro (Eds.), LNCS 5497, pp. 220-239, 2009. A preprint is available on
Open archive preprint, [ bib ].

**Yves Bertot, Ekaterina Komendantskaya**

**Inductive and Coinductive Components of Corecursive Functions in Coq,***ENTCS proceedings of CMCS'08, the 9th International Workshop on Coalgebraic Methods in Computer Science*, Budapest, Hungary, April 4 - April 6, 2008, 20 pages. A preprint is available on
Open archive preprint
[ bib ].

**Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca**

**Canonical Big Operators,***Proceedings of TPHOLs'08*, Springer LNCS 5170, 2008,
Open archive preprint
[ bib ].

**Yves Bertot**

__ Affine functions and series with co-inductive real numbers
__,

**Yves Bertot, Gérard Huet, Jean-Jacques Lévy, Gordon Plotkin (editors)**

__From Semantics to Computer Science, essays in Honour of Gilles Kahn__, Cambridge University Press, 2009, ISBN 978-0-521-51825-3.

**Yves Bertot, Pierre Castéran**

__ Interactive Theorem Proving and Program Development:
Coq'Art: The Calculus of Inductive Constructions__,
Springer Verlag, EATCS Texts in Theoretical Computer Science, 2004, ISBN
3-540-20854-2.
(associated
internet site, Cover of the Chinese
edition, Version
française 2.5MB).
[ bib
]

Yves Bertot