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

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.