[TYPES/announce] Thematic trimester at IHP -- Week 1 -- April 22 to April 26

[Paul-Andre Mellies]

Dear colleagues,

Here follows the program of the first week of the thematic trimester 
« Semantics of Proofs and Certified Mathematics » 
organized at Institut Henri Poincaré in Paris.

The trimester will start by a kick-off afternoon on Tuesday April 22 with

Georges GONTHIER	(Microsoft Research, Cambridge, and MSR-INRIA Joint Centre, Palaiseau)
Thomas HALES	        (University of Pittsburgh)
Xavier LEROY	        (INRIA Paris - Rocquencourt)
Vladimir VOEVODSKY	(Institute for Advanced Study, Princeton)

Two mini-courses will be then given on Wednesday April 23, Thursday April 24 and Friday April 25 by

Gérard BERRY		(Collège de France)
Jean-Yves GIRARD	(CNRS, Institut de Mathématiques de Luminy)

More details on this first week of the thematic trimester will be found below.

The organizers

Pierre-Louis Curien
Hugo Herbelin
Paul-André Melliès

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

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 April 22st – 26th, 2014

TUESDAY APRIL 22nd, 2014

Kick-off afternoon – Amphithéâtre Hermite

Georges GONTHIER	(Microsoft Research, Cambridge, and MSR-INRIA Joint Centre, Palaiseau)
Thomas HALES	        (University of Pittsburgh)
Xavier LEROY	        (INRIA Paris - Rocquencourt)
Vladimir VOEVODSKY	(Institute for Advanced Study, Princeton)

02.00 pm – 02.10pm  :	Semantics of proofs and certified mathematics trimester presentation.
02.10 pm – 02.20 pm :	Welcoming words from Cédric VILLANI the IHP Director.

02.20 pm – 03.10 pm	Georges GONTHIER :
	                                Digitizing the Group Theory of the Odd Order Theorem.

03.10 pm – 04.00 pm	Thomas HALES :
		                        Formalizing the proof of the Kepler Conjecture.

04.00 pm – 04.30 pm 	Coffee break	IHP ground floor

04.30 pm – 05.20 pm	Xavier LEROY :
	                                Proof assistants in computer science research.

05.20 pm – 06.10 pm 	Vladimir VOEVODSKY :
	                                Univalent Foundations - new type-theoretic foundations of mathematics.

06.15 pm 	Cocktail – IHP ground floor


WEDNESDAY APRIL 23rd, 2013

2 pm – 4.30 pm Lecture 1 & 2 (Amphithéâtre Darboux)
Gérard BERRY : Constructive semantics, electricity propagation in circuits, 2-adic numbers, and formal verification.

THURSDAY APRIL 24th, 2014

2 pm – 3 pm Lecture 1 (Amphithéâtre Darboux)
Jean-Yves GIRARD : Qu’est-ce qu’une réponse ? (l'analytique)

3.30 – 4.30 pm Lecture 3 (Amphithéâtre Darboux)
Gérard BERRY : Constructive semantics, electricity propagation in circuits, 2-adic numbers, and formal verification.

FRIDAY APRIL 25th, 2014

2 pm – 3 pm Lecture 2 (Amphithéâtre Darboux)
Jean-Yves GIRARD : Qu’est-ce qu’une question ? (Le format).

3.30 – 4.30 pm Lecture 3 (Amphithéâtre Darboux)
Jean-Yves GIRARD : D’où vient la certitude ? (L’épidictique).

3 pm – 3.30 pm – Tea break on the second floor

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140418/cfc55047/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: kick-off-meeting-22-april.jpg
Type: image/jpg
Size: 142056 bytes
Desc: not available
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140418/cfc55047/attachment-0001.jpg>