Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

start [2014/03/07 13:59]
smimram [IHP Trimester]
start [2014/05/28 09:30] (current)
mellies
Line 26: Line 26:
 ==== Pre-school at the CIRM ==== ==== Pre-school at the CIRM ====
  
-A [[cirm|spring school at CIRM]] is organized from April 7th to April 18th, 2014: If you intend to participate in this event, it will be necessary to [[http://​www.ihp.fr/​en/​ceb/​trimester/​proofs/​cirm|make a pre-registration through this link]]The number of participants to CIRM Spring School being limitedif necessary ​selection among the applications will have to be made by the organisers.+A [[cirm|spring school at CIRM]] is organized from April 7th to April 18th, 2014. Submission for funding is not possible anymorebut few rooms are still available. 
 ==== IHP Trimester ==== ==== IHP Trimester ====
  
Line 32: Line 33:
  
 ^Dates ^Event ^Theme^ ^Dates ^Event ^Theme^
-|22 April|[[kickoff|Kickoff]]|(see below)|+|22 April|[[kickoff|Kickoff]]|**Georges Gonthier**, **Thomas Hales**, **Xavier Leroy** and **Vladimir Voevodsky**|
 |23–25 April|[[Lectures]]|**Gérard Berry** and **Jean-Yves Girard**| |23–25 April|[[Lectures]]|**Gérard Berry** and **Jean-Yves Girard**|
 |28 April|[[industry|Industry]]|**Formal methods for reliable software development in industry**| |28 April|[[industry|Industry]]|**Formal methods for reliable software development in industry**|
-|28 April – 1 May|[[Lectures]]|**François Pottier**, ​**Thorsten Altenkirch** ​and **Jean-Louis Krivine**|+|28–30 April|[[Lectures]]|**Thorsten Altenkirch****Jean-Louis Krivine**, **Per Martin-Löf** and **François Pottier**|
 |5–9 May |[[Workshop 1|Workshop 1]] |**Formalization of mathematics in proof assistants** | |5–9 May |[[Workshop 1|Workshop 1]] |**Formalization of mathematics in proof assistants** |
-|12–16 May|[[http://​www.pps.univ-paris-diderot.fr/​types2014/​|TYPES 2014]]| +|12–16 May|[[http://​www.pps.univ-paris-diderot.fr/​types2014/​|TYPES 2014]]|**TYPES conference**
-|19–20 May|[[federation|Journées]]|**Journées de la Fédération de recherche en mathématiques de Paris-Centre**| +|19–21 May|[[federation|Journées]]|**Journées de la Fédération de recherche en mathématiques de Paris-Centre**| 
-|26–30 May|[[http://​perso.crans.org/​cohen/​map2014/​|MAP 2014]]|+|22–28 May|[[http://​wiki.portal.chalmers.se/​agda/​pmwiki.php?​n=Main.AIMXIX|AIM XIX]]|**19th Agda Implementor'​s Meeting**| 
 +|26–28 May|[[Lectures]]|**Timothy Gowers** and ** Bruno Valette ​**| 
 +|26–30 May|[[http://​perso.crans.org/​cohen/​map2014/​|MAP 2014]]|**Mathematics,​ Algorithms, Proofs conference **|
 |2–6 June |[[Workshop 2]] |**Constructive mathematics and models of type theory** | |2–6 June |[[Workshop 2]] |**Constructive mathematics and models of type theory** |
 |10–14 June |[[Workshop 3]] |**Semantics of proofs and programs** | |10–14 June |[[Workshop 3]] |**Semantics of proofs and programs** |
 +|16–18 June|[[http://​lipn.univ-paris13.fr/​~mazza/​HOComplexity/​|Workshop]]|**Higher order computation:​ types, complexity, applications**|
 +|16–20 June|[[Lectures]]|**Martin Hyland**, **Marc Pouzet**, **Olivier Serre** and **Thomas Streicher**|
 |23–27 June |[[Workshop 4]] |**Abstraction and verification in semantics** | |23–27 June |[[Workshop 4]] |**Abstraction and verification in semantics** |
 +|30 June–4 July|[[Lectures]]|
 |7–11 July |[[Workshop 5]] |**Certification of high-level and low-level programs** | |7–11 July |[[Workshop 5]] |**Certification of high-level and low-level programs** |
  
-==== Kick-off afternoon ==== 
  
-The trimester will begin with a kick-off afternoon on April 22, intended for a large audience of mathematicians and computer scientists. ​ It will consist of 4  talks: +==== Related events hosted at IHP ====
-  * 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//​+
  
-We shall take benefit of the context offered by the thematic to  trimester to organize an afternoon session on //Formal methods for reliable software development in industry// on April 28. The primary aim of the session will be  to give an opportunity to students and academics and non-academic researchers to hear about recent developments of this kind carried out in an industry context. The programme of this afternoon is under elaboration. +  ​* The [[http://​www.pps.univ-paris-diderot.fr/​types2014/​|TYPES 2014]] conference ​was held at IHP on week 4, 12-15 May, followed by the Proof, Computation,​ Complexity workshop
-==== Related events in 2014 ==== +  * The [[http://​wiki.portal.chalmers.se/​agda/​pmwiki.php?​n=Main.AIMXIX|XIX-th Agda Implementors'​ Meeting]] is being held on weeks 5 and 6, 22-28 May.
- +
-  * A five-weeks event on the [[http://​smc2014.univ-lyon1.fr/​|Mathematical Structures of Computation]] is organised in Lyon from January 13th to February 14th, as a progamme of the Laboratoire d'​Excellence MILYON, Together, the two programmes may be considered as a French Semester on certified mathematics,​ programming languages and the mathematical structures of computation. +
-  ​* The [[http://​www.pps.univ-paris-diderot.fr/​types2014/​|TYPES 2014]] conference ​will be held at IHP on week 4, 12-15 May, followed by the Proof, Computation,​ Complexity workshop.+
   * A special edition on constructive mathematics of the [[http://​perso.crans.org/​cohen/​map2014/​|MAP 2014]] conference (Mathematics,​ Algorithms and Proofs) will be held at IHP on week 6, 26-30 May.   * A special edition on constructive mathematics of the [[http://​perso.crans.org/​cohen/​map2014/​|MAP 2014]] conference (Mathematics,​ Algorithms and Proofs) will be held at IHP on week 6, 26-30 May.
   * [[http://​www.bourbaki.ens.fr/​|Bourbaki seminar]] on Saturday 21 June with talks by Thierry Coquand et Thomas Hales.   * [[http://​www.bourbaki.ens.fr/​|Bourbaki seminar]] on Saturday 21 June with talks by Thierry Coquand et Thomas Hales.
 +
 +==== Other related events in 2014 ====
 +
 +  * A five-weeks event on the [[http://​smc2014.univ-lyon1.fr/​|Mathematical Structures of Computation]] was organised in Lyon from January 13th to February 14th, as a progamme of the Laboratoire d'​Excellence MILYON, Together, the two programmes may be considered as a French Semester on certified mathematics,​ programming languages and the mathematical structures of computation.
 +
 +
 ==== Registration ==== ==== Registration ====
  
-**Registration is now open (and free)**. All future ​participants are invited to +**Registration is open and free**. It is requested for logistic reasons. All participants are invited to 
-  -  [[http://​www.ihp.fr/​en/​program/​10226/​register|visit IHP's website to register for the general event]] +  -  [[http://​www.ihp.fr/​en/​program/​10226/​register|visit IHP's website to register for the general event]], mentioning the dates of presence (kick-off, industry afternoon, lectures, workshops 1 to 5) 
-  - and then [[http://​www.ihp.fr/​fr/​program/​10225/​conference/​register|register to the individual workshops]]\\ (please register first to the whole programme above if you intend to participate to one or several of the workshops)+  - workshops 1 to 5 need an [[http://​www.ihp.fr/​fr/​program/​10225/​conference/​register|extra specific registration]] (please register first to the whole programme above if you intend to participate to one or several of the workshops)
 Submission for funding is not possible anymore. Submission for funding is not possible anymore.
  
Line 81: Line 85:
 ==== Sponsors ==== ==== Sponsors ====
  
-{{:​systematic.gif?​nolink&​200|}} +[[http://​www.systematic-paris-region.org/​|{{:​systematic.gif?​nolink&​300|}}]] 
 +[[http://​www.agence-nationale-recherche.fr/​|{{:​anr.png?​100|}}]] 
 +[[http://​recre.ens-lyon.fr/​|{{:​recre.png?​100|}}]]
 ==== Contacts ==== ==== Contacts ====
  
start.1394197178.txt.gz · Last modified: 2014/03/07 13:59 by smimram
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0