[PT] Thematic trimester at IHP - Workshop Formalization of Mathematics in Proof Assistants
Paul-Andre Mellies <mellies-InGYJPFgxhmQrp73wey5nH9PKDog5E0sUBSOeVevoDU@public.gmane.org> Sun, 4 May 2014 18:37:37 +0200
| Newsgroups | gmane.science.mathematics.prooftheory |
|---|---|
| Message-ID | <[email protected]> |
Dear colleagues, We are pleased to announce the workshop « Formalization of Mathematics in Proof Assistants » organized from May 5th to May 9th, 2014 by • Georges Gonthier (Microsoft Research, Cambridge, and Microsoft INRIA Joint Center, Palaiseau) • Vladimir Voevodsky (Institute for Advanced Study, Princeton) This workshop is part of the thematic trimester « Semantics of Proofs and Certified Mathematics » currently held at Institut Henri Poincare. More details will be found on the web site of the trimester: https://ihp2014.pps.univ-paris-diderot.fr/doku.php?id=workshop_1 The organizers Pierre-Louis Curien <curien-InGYJPFgxhmQrp73wey5nH9PKDog5E0sUBSOeVevoDU@public.gmane.org> Hugo Herbelin <[email protected]> Paul-André Melliès <mellies-InGYJPFgxhmQrp73wey5nH9PKDog5E0sUBSOeVevoDU@public.gmane.org> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Thematic program of the Centre Émile Borel « Semantics of Proofs and Certified Mathematics » Paris, April 7th – July 11th, 2014 All the trimester events will take place at IHP, 11 rue Pierre et Marie Curie, Paris 5ème. Program from May 5th – May 9th, 2014 A workshop on « Formalization of Mathematics in Proof Assistants » organized by • Georges Gonthier (Microsoft Research, Cambridge, and Microsoft INRIA Joint Center, Palaiseau) • Vladimir Voevodsky (Institute for Advanced Study, Princeton) == Monday 5 May == 10h00-10h45 Registration 10h45-11h00 Georges Gonthier, Vladimir Voevodsky: Introduction 11h00-12h00 John Harrison: Formal proof: current progress and outstanding challenges 14h00-15h00 Enrico Tassi: Mathematical Components, a large library of formalized mathematics 15h15-16h15 Artur Kornilowicz: Structures and structural types in Mizar 16h45-17h45 Tobias Nipkow: Tame graph enumeration in Flyspeck == Tuesday 6 May == 9h30-10h30 Andrej Bauer, Christopher A. Stone: Brazilian type checking 11h00-12h00 Guillaume Brunerie: Cubical Homotopy Type Theory 14h00-15h00 Benedikt Ahrens: Formalizing category theory in type theory 15h15-16h15 Karol Pak: Formalization of n-dimensional manifolds in Mizar 16h45-17h45 Dan Licata: Eilenberg-MacLane spaces in Homotopy Type Theory == Wednesday 7 May == 9h30-10h30 Thomas Hales: Solovyev's formal computations in HOL Light 11h00-12h00 Daniel Grayson: Formalization of elementary algebraic K-theory in Coq with Univalent Foundations 14h00-15h00 Peter LeFanu Lumsdaine: Recent coherence theorems for dependent type theory 15h15-16h15 Carlos Simpson: Interior/Exterior 16h45-17h45 Urs Schreiber: Classical field theory and Quantization via Cohesive and Linear homotopy types 18h30-21h00 Reception in Jussieu tower == Friday 9 May == 9h30-10h30 Freek Wiedijk: Formal proof done right 11h00-12h00 Norman Megill: The Metamath proof language 14h00-15h00 Bill Richter: Hilbert axiomatic geometry and readable HOL Light proofs 15h15-16h15 Josef Urban: Inductive and deductive AI over large formal libraries 16h45-17h45 Ursula Martin: How do formal proofs happen?