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

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 was available here available here, but this link is only available from within Inria since 2017. A downgraded version 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, Laurence Rideau, Laurent Théry**
Distant decimals of π : Formal proofs of some algorithms computing them and guarantees of exact computation.
*Journal of Automated Reasoning*, December 2017 (open archive version)

**Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub**
Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials Certified Programs and Proofs (CPP'16) (2016), ACM.
(open archive version)

**Yves Bertot**

Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations Certified Programs and Proofs (CPP'15) (2015), ACM. (open archive version)

**Yves Bertot**

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

**Yves Bertot, Guillaume Allais**

__ Views of PI: Definition and computation__
Journal of Formalized Reasoning, Vol 7, No. 1 (2014)

**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, 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), table of contents
sample chapters in English: Chapter 1,Chapter 13,Chapter 14
Chapter 16,
[ bib
].

- A formal description of Fortune's algorithm for Voronoi diagrams.
- Formal proofs for a cell decomposition algorithm.
- formal proofs for the convergence of visibility walks in triangulations
- Motion algorithms for robots
- Formal proofs of absence of collisions for Bézier curves
- Formal proofs of absence of collisions for broken line trajectories