Yves Bertot's guest appearances

Yves Bertot

CAST IT (audio)

CAST IT (video)

Type Theory Forall

Robin Hanson

Rebecca Slayton

Ivan Damgård

Tim Roughgarden

Claire Mathieu

Toby Walsh

Espen Aarseth

Troels Bjerre Lund

Carsten Schürmann

Chris Jenkins

Eric Bond

Anupam Das

Conal Elliott

John Wiegley

OwlTail

In this episode we interview Yves Bertot and we talk about the history behind his contribution with Pierre Castéran on writing Coq’Art. What is Yves’ role in the Coq Team, how the team works and what are the sort of contributions they accept. Links: Yves email: yves.bertot@inria.fr Affichage et manipulation interactive de formules mathématiques dans les documents structurés - Check figure 15 for an example on how Yves’ tools would build trees internally A video showing his tool in practice, doing proofs with mouse clicks A Genereic Approach to Building User Interfaces for Theorem Provers

In this episode we interview Yves Bertot and we talk about the history behind his contribution with Pierre Castéran on writing Coq’Art. What is Yves’ role in the Coq Team, how the team works and what are the sort of contributions they accept. Links: <a href="mailto:yves.bertot@inria.fr" rel="nofollow noopener noreferrer">Yves email: yves.bertot@inria.fr</a> <a href="https://www.typetheoryforall.com/docs/Yves-sqrt.pdf" rel="nofollow noopener noreferrer" target="_blank">Affichage et manipulation interactive de formules mathématiques dans les documents structurés</a> - Check figure 15 for an example on how Yves’ tools would build trees internally <a href="https://www.typetheoryforall.com/docs/Yves-proof.mkv" rel="nofollow noopener noreferrer" target="_blank">A video showing his tool in practice, doing proofs with mouse clicks</a> <a href="https://www.semanticscholar.org/paper/A-Generic-Approach-to-Building-User-Interfaces-for-Bertot-Th%C3%A9ry/64d8d7c01d2ec4a6dda839ff506a97d04bcd9829" rel="nofollow noopener noreferrer" target="_blank">A Genereic Approach to Building User Interfaces for Theorem Provers</a>

#5 The History of Coq'Art - Yves Bertot

Yves Bertot is a senior researcher that the French Institute for Research in Computer Science and Automation (INRIA) in Sophia Antipolis and a leading researcher on correctness of software and the verification of mathematical proofs. Recently, his team was able to formally verify the correctness of the computation on the one millionth decimal digit of pi (which is 1, by the way), including a formally verifiable proof of the mathematics behind the formula and the correctness of the implementation of arithmetic operations used in the computation. We use this result as an inspiration to talk about interactive theorem proving and improving software quality.Yves’ book with Pierre Casterán about interactive theorem proving using the Coq system is “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.

Yves Bertot is a senior researcher that the French Institute for Research in Computer Science and Automation (INRIA) in Sophia Antipolis and a leading researcher on correctness of software and the verification of mathematical proofs. Recently, his team was able to formally verify the correctness of the computation on the one millionth decimal digit of pi (which is 1, by the way), including a formally verifiable proof of the mathematics behind the formula and the correctness of the implementation of arithmetic operations used in the computation. We use this result as an inspiration to talk about interactive theorem proving and improving software quality. Yves’ book with Pierre Casterán about interactive theorem proving using the Coq system is “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.

Yves Bertot: Verifying One Million Digits of Pi