Registration
This shows you the differences between two versions of the page.
|
kickoff [2014/03/12 16:06] smimram [Planning] |
kickoff [2014/04/01 23:02] (current) smimram [Planning] |
||
|---|---|---|---|
| Line 6: | Line 6: | ||
| * **Xavier Leroy** (INRIA Paris-Rocquencourt): //Proof assistants in computer science research// | * **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// | * **Vladimir Voevodsky** (Institute for Advanced Study, Princeton): //Univalent Foundations - new type-theoretic foundations of mathematics// | ||
| - | |||
| - | We shall take benefit of the context offered by the thematic to trimester to organize an afternoon session on //Formal methods for reliable software development in industry// on April 28. The primary aim of the session will be to give an opportunity to students and academics and non-academic researchers to hear about recent developments of this kind carried out in an industry context. The programme of this afternoon is under elaboration. | ||
| ===== Planning ===== | ===== Planning ===== | ||
| - | |14h-15h|Gonthier|Group Theory of the Odd Order Theorem| | + | |14h-14h10 |« Semantics of proofs and certified mathematics » trimester presentation|| |
| - | |15h-16h|Hales| | + | |14h-14h20 |Welcoming words from Cédric Villani the IHP Director|| |
| - | |16h-16h30|//pause//| | + | |14h20-15h10 |Georges Gonthier |Digitizing the Group Theory of the Odd Order Theorem| |
| - | |16h30-17h30|Leroy| | + | |15h10-16h |Thomas Hales |Formalizing the proof of the Kepler Conjecture| |
| - | |17h30-18h30|Voevodsky| | + | |16h-16h30 |//break//|| |
| - | |18h30|//cocktail//| | + | |16h30-17h20 |Xavier Leroy |Proof assistants in computer science research| |
| + | |17h20-18h10 |Vladimir Voevodsky |Univalent Foundations - new type-theoretic foundations of mathematics| | ||
| + | |18h15 |//cocktail//|| | ||