We are glad to announce the kick-off meeting of the thematic trimester
** Semantics of proofs and certified mathematics **
which will be held at Institut Henri Poincarι (IHP), Paris, on the afternoon of Tuesday, April 22, 2014.
Four keynote speakers are invited to give a talk on this occasion:
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
More information on the thematic trimester will be found on the webpage
https://ihp2014.pps.univ-paris-diderot.fr/doku.phpYou will find preliminary lists of confirmed invited speakers for the 5 workshops of the IHP programme
59 May
Workshop 1
Formalization of mathematics in proof assistants