Dear all, 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.php You will find preliminary lists of confirmed invited speakers for the 5 workshops of the IHP programme 5–9 May Workshop 1 Formalization of mathematics in proof assistants 2–6 June Workshop 2 Constructive mathematics and models of type theory 10–14 June Workshop 3 Semantics of proofs and programs 23–27 June Workshop 4 Abstraction and verification in semantics 7–11 July Workshop 5 Certification of high-level and low-level programs Registration to individual workshops is free but mandatory here: http://www.ihp.fr/en/ceb/trimester/proofs (you do not need to register to the trimester unless you intend to stay for longer than the duration of a workshop) https://webmail.pps.univ-paris-diderot.fr/SOGo/so/curien/Mail/0/folderDrafts... The organisers Pierre-Louis Curien <curien@pps.univ-paris-diderot.fr> Hugo Herbelin <Hugo.Herbelin@inria.fr> Paul-Andre Mellies <mellies@pps.univ-paris-diderot.fr> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]