T2-2014 : Semantics of proofs and certified mathematics

# You can also click the upper-left icon to select videos from the playlist.

source: Institut Henri Poincaré     2014年4月22日
T2-2014 : Semantics of proofs and certified mathematics
Institut Henri Poincaré thematic trimester
Program and registration : https://ihp2014.pps.univ-paris-diderot.fr/
After years of steady development, the technology of proof assistants is currently coming to a mature state. As a matter of fact, it is possible today to formalize a non trivial mathematical proof inside a computer, and to check its correctness automatically. This "tour de force" has been recently achieved for the four color theorem, and a certified proof of the classification of finite groups and of the Kepler conjecture are on the way.
These achievements would not have been possible without the rich and active mathematics of formal proofs which emerged in the 1970s at the frontier of logic and computer science, along the Curry-Howard correspondence. This seminal correspondence enables us to understand a logical proof (of a given formula) as a well-behaved program (of a given type). Besides this by now traditional connection between logic and computer science, a number of unexpected connections are currently emerging with other fields of mathematics -- this including homotopy theory, higher dimensional algebra, quantum topology, topos theory, functional analysis and operator algebra. Finally, proof assistants have been successfully applied to certify properties of programs written in high-level languages as well as low-level languages, to implement certified compilers, or to establish important security properties of protocols.
The purpose of this thematic trimester is to provide a forum for the extended community of researchers and students in mathematics and in computer science interested in proof assistants, and more generally, in the mathematics of formal proofs. Much care will be devoted during the trimester to train the mathematicians interested to learn and to use the current proof assistants in their work.

1 - Kick-off afternoon : introduction and welcoming word by Cédric Villani 20:25
2 - Kick-off afternoon : Georges Gonthier, Digitizing the Group Theory of the Odd Order Theorem 40:32
3 - Kick-off afternoon : Thomas Hales, Formalizing the proof of the Kepler Conjecture 43:18
4 - Kick-off afternoon : Xavier Leroy, Proof assistants in computer science research 50:30
5 - Kick-off afternoon : Vladimir Voevodsky, Univalent Foundations 54:16
6 - Lectures - Gérard Berry, Constructive semantics, electricity propagation in circuits... 1/2 2:13:02
7 - Lectures - Gérard Berry, Constructive semantics, electricity propagation in circuits... 2/2 1:00:17
8 - Lectures : Jean-Yves Girard 1/3, Qu'est-ce qu'une réponse ? (l'analytique) 1:03:58
9 - Lectures : Jean-Yves Girard 2/3, Qu'est-ce qu'une question ? (le format) 1:04:53
10 - Lectures : Jean-Yves Girard 3/3, D'où vient la certitude ? (l'épidictique) 1:17:27
Jean Louis Krivine - 1/2 La correspondance de Curry-Howard donne de nouveaux modèles de ZF 1:35:58
Jean Louis Krivine - 2/2 Curry-Howard correspondence gives new models of ZF 1:44:15
François Potier - 1/2 The practice and theory of Mezzo 1:36:03
François Potier - 2/2 The practice and theory of Mezzo 1:35:44
Thorsten Altenkirch - 1/2 Towards a Syntax for Cubical Type Theory 1:17:33
Thorsten Altenkirch - 2/2 Towards a Syntax for Cubical Type Theory 59:32