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:
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.
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 Interactive Theorem Proving, Springer Verlag, LNCS 7998, pp. 163-179, 2013. Open archive preprint
Yves Bertot, Frédérique Guilhot, Assia
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
Formal proof of theorems on genetic regulatory networks In Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2009), pages 69-76. IEEE, September 2009.
Theorem-Proving Support in programming language semantics, From Semantics to Computer Science, essays in Honour of Gilles Kahn, Cambridge University Press, 2009. Open archive preprint [ bib].
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]
Structural Abstract Interpretation: A Formal Study Using Coq, Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised Tutorial Lectures, Springer Verlag, LNCS 5520, pp. 153-194, 2009. Open archive preprint (less errors), [ bib ].
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 ].
Affine functions and series with co-inductive real numbers , Mathematical Structures in Computer Science, 17(1):37-63 (2007),Cambridge University Press, Open archive preprint [ bib ]
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 ]