IT University of Copenhagen sitecore@itu.dk https://video.itu.dk en-us Visualplatform http://blogs.law.harvard.edu/tech/rss IT University of Copenhagen Stay up to date with all the things that are happening at IT University of Copenhagen. This podcast will serve you various videos and audios with accounts from scientists and actual students at IT University, and give you a glimpse into their... episodic no https://video.itu.dk/files/rv0.0/sitelogo.gif https://video.itu.dk http://video.itu.dk/photo/27249551/yves-bertot-verifying-one-million <p>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. <p>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.</p></p><p><a href="http://video.itu.dk/photo/27249551/yves-bertot-verifying-one-million"><img src="http://video.itu.dk/7718128/27249551/ae8c83a9a4a8118efbc126daafa82d3d/standard/download-2-thumbnail.jpg" width="600" height="338"/></a></p> http://video.itu.dk/photo/27249551 Thu, 19 Apr 2018 15:23:29 GMT Yves Bertot: Verifying One Million Digits of Pi 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... IT University of Copenhagen 01:07:38 <p>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. <p>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.</p></p><p><a href="http://video.itu.dk/photo/27249551/yves-bertot-verifying-one-million"><img src="http://video.itu.dk/7718128/27249551/ae8c83a9a4a8118efbc126daafa82d3d/standard/download-2-thumbnail.jpg" width="600" height="338"/></a></p> cast it computation one millionth digit of pi