Registration
This shows you the differences between two versions of the page.
|
kickoff [2014/02/20 09:52] smimram created |
kickoff [2014/04/01 23:02] (current) smimram [Planning] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ~~REDIRECT>start~~ | + | ====== Kick-off afternoon ====== |
| + | |||
| + | 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: | ||
| + | * **Georges Gonthier** (Microsoft Research, Cambridge, and Microsoft INRIA Joint Center, Palaiseau): //Digitizing the Group Theory of the Odd Order Theorem// | ||
| + | * **Thomas Hales** (University of Pittsburgh): //Formalizing the proof of the Kepler Conjecture// | ||
| + | * **Xavier Leroy** (INRIA Paris-Rocquencourt): //Proof assistants in computer science research// | ||
| + | * **Vladimir Voevodsky** (Institute for Advanced Study, Princeton): //Univalent Foundations - new type-theoretic foundations of mathematics// | ||
| + | |||
| + | ===== Planning ===== | ||
| + | |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//|| | ||