Registration
The trimester will begin with a kick-off afternoon on April 22, intended for a large audience of mathematicians and computer scientists. It will consist of 4 talks:
14h-14h10 | « Semantics of proofs and certified mathematics » trimester presentation | |
14h-14h20 | Welcoming words from Cédric Villani the IHP Director | |
14h20-15h10 | Georges Gonthier | Digitizing the Group Theory of the Odd Order Theorem |
15h10-16h | Thomas Hales | Formalizing the proof of the Kepler Conjecture |
16h-16h30 | break | |
16h30-17h20 | Xavier Leroy | Proof assistants in computer science research |
17h20-18h10 | Vladimir Voevodsky | Univalent Foundations - new type-theoretic foundations of mathematics |
18h15 | cocktail |