---------- Forwarded message ----------
From: Paul-Andre Mellies <[email protected]>
Date: 2014-04-18 5:20 GMT-03:00
Subject: [TYPES/announce] Thematic trimester at IHP -- Week 1 -- April 22
to April 26
To: [email protected]
[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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)
J*ean-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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
_______________________________________________
Logica-l mailing list
[email protected]
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
