Completed
1 - Kick-off afternoon : introduction and welcoming word by Cédric Villani
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Semantics of Proofs and Certified Mathematics
Automatically move to the next video in the Classroom when playback concludes
- 1 1 - Kick-off afternoon : introduction and welcoming word by Cédric Villani
- 2 2 - Kick-off afternoon : Georges Gonthier, Digitizing the Group Theory of the Odd Order Theorem
- 3 3 - Kick-off afternoon : Thomas Hales, Formalizing the proof of the Kepler Conjecture
- 4 4 - Kick-off afternoon : Xavier Leroy, Proof assistants in computer science research
- 5 5 - Kick-off afternoon : Vladimir Voevodsky, Univalent Foundations
- 6 6 - Lectures - Gérard Berry, Constructive semantics, electricity propagation in circuits... 1/2
- 7 7 - Lectures - Gérard Berry, Constructive semantics, electricity propagation in circuits... 2/2
- 8 8 - Lectures : Jean-Yves Girard 1/3, Qu'est-ce qu'une réponse ? (l'analytique)
- 9 9 - Lectures : Jean-Yves Girard 2/3, Qu'est-ce qu'une question ? (le format)
- 10 10 - Lectures : Jean-Yves Girard 3/3, D'où vient la certitude ? (l'épidictique)
- 11 Jean Louis Krivine - 1/2 La correspondance de Curry-Howard donne de nouveaux modèles de ZF
- 12 Jean Louis Krivine - 2/2 Curry-Howard correspondence gives new models of ZF
- 13 François Potier - 1/2 The practice and theory of Mezzo
- 14 François Potier - 2/2 The practice and theory of Mezzo
- 15 Thorsten Altenkirch - 1/2 Towards a Syntax for Cubical Type Theory
- 16 Thorsten Altenkirch - 2/2 Towards a Syntax for Cubical Type Theory
