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

cirm [2013/10/15 00:13]
smimram
cirm [2014/03/31 17:06] (current)
smimram [Second week]
Line 12: Line 12:
 This two week school is aimed as an intensive preparation and training for PhD students and master students who will participate to the IHP program, starting right after the two week school at the CIRM and running until mid July, 2014. This two week school is aimed as an intensive preparation and training for PhD students and master students who will participate to the IHP program, starting right after the two week school at the CIRM and running until mid July, 2014.
  
-==== Week 1 ====+==== First week ==== 
 +^Monday 07 April 2014||| 
 +|09:30 - 10:​30|Thierry Coquand|Constructive mathematics and homotopy type theory ​1
 +|//Coffee Break//​||| 
 +|11:00 - 12:​00|Thierry Coquand|Constructive mathematics and homotopy type theory 2| 
 +|//​Lunch//​||| 
 +|14:00 - 15:00|Assia Mahboubi|Formalization of mathematics in proof assistants 1| 
 +|//Coffee Break//​||| 
 +|15:30 - 16:30|Assia Mahboubi|Formalization of mathematics in proof assistants 2| 
 +|17:00 - 18:​00|Working groups and exercises|| 
 +|//​Dinner//​||| 
 + 
 +^Tuesday 08 April 2014||| 
 +|09:30 - 10:​30|Thierry Coquand|Constructive mathematics and homotopy type theory 3| 
 +|//Coffee Break//​||| 
 +|11:00 - 12:​00|Thierry Coquand|Constructive mathematics and homotopy type theory 4| 
 +|//​Lunch//​||| 
 +|14:00 - 15:00|Assia Mahboubi|Formalization of mathematics in proof assistants 3| 
 +|//Coffee Break//​||| 
 +|15:30 - 16:30|Assia Mahboubi|Formalization of mathematics in proof assistants 4| 
 +|17:00 - 18:​00|Working groups and exercises|| 
 +|//​Dinner//​||| 
 + 
 +^Wednesday 09 April 2014||| 
 +|09:30 - 10:​30|Alexandre Miquel|Computational interpretation of proofs and realizability 1| 
 +|//Coffee Break//​||| 
 +|11:00 - 12:​00|Alexandre Miquel|Computational interpretation of proofs and realizability 2| 
 +|//Lunch and free afternoon//​||| 
 + 
 +^Thursday 10 April 2014||| 
 +|09:30 - 10:​30|Alexandre Miquel|Computational interpretation of proofs and realizability 3| 
 +|//Coffee Break//​||| 
 +|11:00 - 12:​00|Alexandre Miquel|Computational interpretation of proofs and realizability 4| 
 +|//​Lunch//​| 
 +|14:00 - 15:00|Assia Mahboubi|Formalization of mathematics in proof assistants 5| 
 +|//Coffee Break//​||| 
 +|15:30 - 16:30|Assia Mahboubi|Formalization of mathematics in proof assistants 6| 
 +|17:00 - 18:​00|Working groups and exercises|| 
 +|//Social dinner (bouillabaisse) (CIRM Marseille)//​||| 
 + 
 +^Friday 11 April 2014||| 
 +|09:30 - 10:​30|Thierry Coquand|Constructive mathematics and homotopy type theory 5| 
 +|//Coffee Break//​||| 
 +|11:00 - 12:​00|Thierry Coquand|Constructive mathematics and homotopy type theory 6| 
 +|//​Lunch//​||| 
 +|14:00 - 15:​00|Alexandre Miquel|Computational interpretation of proofs and realizability 5| 
 +|//Coffee Break//​||| 
 +|15:30 - 16:​30|Alexandre Miquel|Computational interpretation of proofs and realizability 6| 
 +|//​Dinner//​| 
 + 
 +^Saturday 12 April 2014||| 
 +|//Lunch (CIRM Marseille)//​||| 
 + 
 +==== Second week ==== 
 +^Monday 14 April 2014||| 
 +|09:30 - 10:​30|Pierre-Louis Curien|Linear logic, game semantics and environment machines 1| 
 +|Coffee Break||| 
 +|11:00 - 12:​00|Pierre-Louis Curien|Linear logic, game semantics and environment machines 2| 
 +|//​Lunch//​||| 
 +|14:00 - 15:00|Alex Simpson|Semantics of programming languages with effects 1| 
 +|//Coffee Break//| 
 +|15:30 - 16:30|Alex Simpson|Semantics of programming languages with effects 2| 
 +|17:00 - 18:​00|Working groups and exercises|| 
 +|//​Dinner//​||| 
 + 
 +^Tuesday 15 April 2014||| 
 +|09:30 - 10:​30|Pierre-Louis Curien|Linear logic, game semantics and environment machines 3| 
 +|//Coffee Break//​||| 
 +|11:00 - 12:​00|Pierre-Louis Curien|Linear logic, game semantics and environment machines 4| 
 +|//​Lunch//​||| 
 +|14:00 - 15:00|Alex Simpson|Semantics of programming languages with effects 3| 
 +|//Coffee Break//​||| 
 +|15:30 - 16:30|Alex Simpson|Semantics of programming languages with effects 4| 
 +|17:00 - 18:​00|Working groups and exercises|| 
 +|//​Dinner//​||| 
 + 
 +^Wednesday 16 April 2014||| 
 +|09:30 - 10:30|Amal Ahmed|Syntax and semantics of low level languages 1| 
 +|//Coffee Break//​||| 
 +|11:00 - 12:00|Amal Ahmed|Syntax and semantics of low level languages 2| 
 +|//Lunch and free afternoon//​||| 
 + 
 +^Thursday 17 April 2014||| 
 +|09:30 - 10:​30|Pierre-Louis Curien|Linear logic, game semantics and environment machines 5| 
 +|//Coffee Break//​||| 
 +|11:00 - 12:​00|Pierre-Louis Curien|Linear logic, game semantics and environment machines 6| 
 +|//​Lunch//​| 
 +|14:00 - 15:00|Amal Ahmed|Syntax and semantics of low level languages 3| 
 +|//Coffee Break (CIRM Marseille)//​||| 
 +|15:30 - 16:30|Amal Ahmed|Syntax and semantics of low level languages 4| 
 +|17:00 - 18:​00|Working groups and exercises|| 
 +|//Social dinner (bouillabaisse) (CIRM Marseille)//​||| 
 + 
 +^Friday 18 April 2014||| 
 +|09:30 - 10:30|Alex Simpson|Semantics of programming languages with effects 5| 
 +|//Coffee Break//​||| 
 +|11:00 - 12:00|Alex Simpson|Semantics of programming languages with effects 6| 
 +|//​Lunch//​||| 
 +|14:00 - 15:00|Amal Ahmed|Syntax and semantics of low level languages 5| 
 +|//Coffee Break//​||| 
 +|15:30 - 16:30|Amal Ahmed|Syntax and semantics of low level languages 6| 
 +|//Dinner (CIRM Marseille)//​||| 
 +===== Talks ===== 
 +==== First week ====
 From 7 to 11 April 2014. From 7 to 11 April 2014.
-  * A 6-hour intensive course on **constructive mathematics and homotopy type theory** by //Thierry Coquand// (Chalmers University):​ principles of constructive mathematics,​ Curry-Howard correspondence,​ typed λ-calculi, Martin-Löf type theory, homotopy type theory, univalence axiom, proof-irrelevance. +  * A 6-hour intensive course on **constructive mathematics and homotopy type theory** by //Thierry Coquand// (Chalmers University, Gothenburg): principles of constructive mathematics,​ Curry-Howard correspondence,​ typed λ-calculi, Martin-Löf type theory, homotopy type theory, univalence axiom, proof-irrelevance. 
-  * A 6-hour intensive course on **formalization of mathematics in proof assistants** by //Assiah ​Mahboubi// (INRIA, LIX, Ecole Polytechnique): introduction to the theoretical as well as the practical aspects of formalization,​ with illustrations on the proof assistant Coq. +  * A 6-hour intensive course on **formalization of mathematics in proof assistants** by //Assia Mahboubi// (INRIA ​Saclay): introduction to the theoretical as well as the practical aspects of formalization,​ with illustrations on the proof assistant Coq. 
-  * A 6-hour intensive course on **computational interpretation of proofs and realizability** by //Alexandre Miquel// (LIPENS Lyon): continuation-passing style translations,​ Kripke semantics, Kleene realizability,​ forcing and models of set-theory, Krivine classical realizability.+  * A 6-hour intensive course on **computational interpretation of proofs and realizability** by //Alexandre Miquel// (Universidad de la RepúblicaMontevideo): continuation-passing style translations,​ Kripke semantics, Kleene realizability,​ forcing and models of set-theory, Krivine classical realizability.
   * Discussion sessions as well as practical sessions on the computer.   * Discussion sessions as well as practical sessions on the computer.
  
-==== Week 2 ====+==== Second week ====
 From 14 to 18 April 2014. From 14 to 18 April 2014.
   * A 6-hour intensive course on the **syntax and semantics of low level languages** by //Amal Ahmed// (Northeastern University):​ principles of von Neuman architecture,​ typed assembly languages, Hoare logic, separation logic, semantic study of the heap, higher order referenes, logical relations, forcing, step-indexing techniques.   * A 6-hour intensive course on the **syntax and semantics of low level languages** by //Amal Ahmed// (Northeastern University):​ principles of von Neuman architecture,​ typed assembly languages, Hoare logic, separation logic, semantic study of the heap, higher order referenes, logical relations, forcing, step-indexing techniques.
   * A 6-hour intensive course on **linear logic, game semantics and environment machines** by //​Pierre-Louis Curien// (CNRS, PPS, Universté Paris Diderot): basics of category theory, monads and adjunctions,​ abstract machines, linear logic, constructive classical logic, denotation of proofs and programs (Scott domains, game semantics).   * A 6-hour intensive course on **linear logic, game semantics and environment machines** by //​Pierre-Louis Curien// (CNRS, PPS, Universté Paris Diderot): basics of category theory, monads and adjunctions,​ abstract machines, linear logic, constructive classical logic, denotation of proofs and programs (Scott domains, game semantics).
-  * A 6-hour intensive course on the **semantics of programming languages with effects** by //Alex Simpson// (LFCS, University of Edinburgh): computational monads, ​Lawvere theories, combining monads, algebraic ​vs. observational ​theory of effects, ​sheaf-models of local storesmonads with arities.+  * A 6-hour intensive course on the **semantics of programming languages with effects** by //Alex Simpson// (LFCS, University of Edinburgh): computational ​effects and monads, ​metalanaguages for effects, algebraic theory of effects, ​continuations,​ presheaf ​models of local storeobservations and modalities.
   * Discussion sessions as well as practical sessions on the computer.   * Discussion sessions as well as practical sessions on the computer.
- 
 ===== Organizers ===== ===== Organizers =====
   * [[curien@pps.univ-paris-diderot.fr|Pierre-Louis Curien]], directeur de recherche CNRS, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot   * [[curien@pps.univ-paris-diderot.fr|Pierre-Louis Curien]], directeur de recherche CNRS, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot
   * [[herbelin@pps.univ-paris-diderot.fr|Hugo Herbelin]], directeur de recherche INRIA, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot   * [[herbelin@pps.univ-paris-diderot.fr|Hugo Herbelin]], directeur de recherche INRIA, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot
   * [[mellies@pps.univ-paris-diderot.fr|Paul-André Melliès]], chargé de recherche CNRS, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot   * [[mellies@pps.univ-paris-diderot.fr|Paul-André Melliès]], chargé de recherche CNRS, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot
cirm.1381788830.txt.gz · Last modified: 2013/10/15 00:13 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