[TYPES/announce] Thematic trimester at IHP - Workshop Formalization of Mathematics in Proof Assistants

[Paul-Andre Mellies]

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 at pps.univ-paris-diderot.fr>
Hugo Herbelin <herbelin at inria.fr>
Paul-André Melliès <mellies at pps.univ-paris-diderot.fr>

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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?


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140503/56dd2188/attachment.html>