Registration

Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

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

cirm [2014/03/07 14:54] smimram [Programme] |
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. | ||

+ | ==== First week ==== | ||

^Monday 07 April 2014||| | ^Monday 07 April 2014||| | ||

|09:30 - 10:30|Thierry Coquand|Constructive mathematics and homotopy type theory 1| | |09:30 - 10:30|Thierry Coquand|Constructive mathematics and homotopy type theory 1| | ||

Line 51: | Line 52: | ||

|//Social dinner (bouillabaisse) (CIRM Marseille)//||| | |//Social dinner (bouillabaisse) (CIRM Marseille)//||| | ||

- | === Friday 11 April 2014 | + | ^Friday 11 April 2014||| |

- | Friday 11 April 2014 09:30 - 10:30 | + | |09:30 - 10:30|Thierry Coquand|Constructive mathematics and homotopy type theory 5| |

- | Thierry Coquand "Constructive mathematics and homotopy type theory" 5 | + | |//Coffee Break//||| |

- | Friday 11 April 2014 10:30 - 11:00 | + | |11:00 - 12:00|Thierry Coquand|Constructive mathematics and homotopy type theory 6| |

- | Coffee Break | + | |//Lunch//||| |

- | Friday 11 April 2014 11:00 - 12:00 | + | |14:00 - 15:00|Alexandre Miquel|Computational interpretation of proofs and realizability 5| |

- | Thierry Coquand "Constructive mathematics and homotopy type theory" 6 | + | |//Coffee Break//||| |

- | Friday 11 April 2014 12:00 - 14:00 | + | |15:30 - 16:30|Alexandre Miquel|Computational interpretation of proofs and realizability 6| |

- | Lunch | + | |//Dinner//| |

- | Friday 11 April 2014 14:00 - 15:00 | + | |

- | Alexandre Miquel "Computational interpretation of proofs and = | + | |

- | realizability" 5 | + | |

- | Friday 11 April 2014 15:00 - 15:30 | + | |

- | Coffee Break | + | |

- | Friday 11 April 2014 15:30 - 16:30 | + | |

- | Alexandre Miquel "Computational interpretation of proofs and = | + | |

- | realizability" 6 | + | |

- | Friday 11 April 2014 19:30 - 21:00 | + | |

- | Dinner | + | |

- | === Saturday 12 April 2014 | + | ^Saturday 12 April 2014||| |

- | Saturday 12 April 2014 12:00 - 13:00 | + | |//Lunch (CIRM Marseille)//||| |

- | Lunch (CIRM Marseille) | + | |

- | === Monday 14 April 2014 09:30 - 10:30 | + | ==== Second week ==== |

- | Pierre-Louis Curien "Linear logic, game semantics and environment = | + | ^Monday 14 April 2014||| |

- | machines" 1 | + | |09:30 - 10:30|Pierre-Louis Curien|Linear logic, game semantics and environment machines 1| |

- | Monday 14 April 2014 10:30 - 11:00 | + | |Coffee Break||| |

- | Coffee Break | + | |11:00 - 12:00|Pierre-Louis Curien|Linear logic, game semantics and environment machines 2| |

- | Monday 14 April 2014 11:00 - 12:00 | + | |//Lunch//||| |

- | Pierre-Louis Curien "Linear logic, game semantics and environment = | + | |14:00 - 15:00|Alex Simpson|Semantics of programming languages with effects 1| |

- | machines" 2 | + | |//Coffee Break//| |

- | Monday 14 April 2014 12:00 - 14:00 | + | |15:30 - 16:30|Alex Simpson|Semantics of programming languages with effects 2| |

- | Lunch | + | |17:00 - 18:00|Working groups and exercises|| |

- | Monday 14 April 2014 14:00 - 15:00 | + | |//Dinner//||| |

- | Alex Simpson "Semantics of programming languages with effects" 1 | + | |

- | Monday 14 April 2014 15:00 - 15:30 | + | |

- | Coffee Break | + | |

- | Monday 14 April 2014 15:30 - 16:30 | + | |

- | Alex Simpson "Semantics of programming languages with effects" 2 | + | |

- | Monday 14 April 2014 17:00 - 18:00 | + | |

- | Working groups and exercises | + | |

- | Monday 14 April 2014 19:30 - 21:00 | + | |

- | Dinner | + | |

- | === Tuesday 15 April 2014 | + | ^Tuesday 15 April 2014||| |

- | Tuesday 15 April 2014 09:30 - 10:30 | + | |09:30 - 10:30|Pierre-Louis Curien|Linear logic, game semantics and environment machines 3| |

- | Pierre-Louis Curien "Linear logic, game semantics and environment = | + | |//Coffee Break//||| |

- | machines" 3 | + | |11:00 - 12:00|Pierre-Louis Curien|Linear logic, game semantics and environment machines 4| |

- | Tuesday 15 April 2014 10:30 - 11:00 | + | |//Lunch//||| |

- | Coffee Break | + | |14:00 - 15:00|Alex Simpson|Semantics of programming languages with effects 3| |

- | Tuesday 15 April 2014 11:00 - 12:00 | + | |//Coffee Break//||| |

- | Pierre-Louis Curien "Linear logic, game semantics and environment = | + | |15:30 - 16:30|Alex Simpson|Semantics of programming languages with effects 4| |

- | machines" 4 | + | |17:00 - 18:00|Working groups and exercises|| |

- | Tuesday 15 April 2014 12:00 - 14:00 | + | |//Dinner//||| |

- | Lunch | + | |

- | Tuesday 15 April 2014 14:00 - 15:00 | + | |

- | Alex Simpson "Semantics of programming languages with effects" 3 | + | |

- | Tuesday 15 April 2014 15:00 - 15:30 | + | |

- | Coffee Break | + | |

- | Tuesday 15 April 2014 15:30 - 16:30 | + | |

- | Alex Simpson "Semantics of programming languages with effects" 4 | + | |

- | Tuesday 15 April 2014 17:00 - 18:00 | + | |

- | Working groups and exercises | + | |

- | Tuesday 15 April 2014 19:30 - 21:00 | + | |

- | Dinner | + | |

- | === Wednesday 16 April 2014 | + | ^Wednesday 16 April 2014||| |

- | Wednesday 16 April 2014 09:30 - 10:30 | + | |09:30 - 10:30|Amal Ahmed|Syntax and semantics of low level languages 1| |

- | Amal Ahmed "Syntax and semantics of low level languages" 1 | + | |//Coffee Break//||| |

- | Wednesday 16 April 2014 10:30 - 11:00 | + | |11:00 - 12:00|Amal Ahmed|Syntax and semantics of low level languages 2| |

- | Coffee Break | + | |//Lunch and free afternoon//||| |

- | Wednesday 16 April 2014 11:00 - 12:00 | + | |

- | Amal Ahmed "Syntax and semantics of low level languages" 2 | + | |

- | Wednesday 16 April 2014 12:00 - 14:00 | + | |

- | Lunch | + | |

- | Wednesday 16 April 2014 19:30 - 21:00 | + | |

- | Dinner | + | |

- | === Thursday 17 April 2014 | + | ^Thursday 17 April 2014||| |

- | Thursday 17 April 2014 09:30 - 10:30 | + | |09:30 - 10:30|Pierre-Louis Curien|Linear logic, game semantics and environment machines 5| |

- | Pierre-Louis Curien "Linear logic, game semantics and environment = | + | |//Coffee Break//||| |

- | machines" 5 | + | |11:00 - 12:00|Pierre-Louis Curien|Linear logic, game semantics and environment machines 6| |

- | Thursday 17 April 2014 10:30 - 11:00 | + | |//Lunch//| |

- | Coffee Break | + | |14:00 - 15:00|Amal Ahmed|Syntax and semantics of low level languages 3| |

- | Thursday 17 April 2014 11:00 - 12:00 | + | |//Coffee Break (CIRM Marseille)//||| |

- | Pierre-Louis Curien "Linear logic, game semantics and environment = | + | |15:30 - 16:30|Amal Ahmed|Syntax and semantics of low level languages 4| |

- | machines" 6 | + | |17:00 - 18:00|Working groups and exercises|| |

- | Thursday 17 April 2014 12:00 - 14:00 | + | |//Social dinner (bouillabaisse) (CIRM Marseille)//||| |

- | Lunch | + | |

- | Thursday 17 April 2014 14:00 - 15:00 | + | |

- | Amal Ahmed "Syntax and semantics of low level languages" 3 | + | |

- | Thursday 17 April 2014 15:00 - 15:30 | + | |

- | Coffee Break (CIRM Marseille) | + | |

- | Thursday 17 April 2014 15:30 - 16:30 | + | |

- | Amal Ahmed "Syntax and semantics of low level languages" 4 | + | |

- | Thursday 17 April 2014 17:00 - 18:00 | + | |

- | Working groups and exercises | + | |

- | Thursday 17 April 2014 19:30 - 22:00 | + | |

- | Social dinner (bouillabaisse) (CIRM Marseille) | + | |

- | === Friday 18 April 2014 | + | ^Friday 18 April 2014||| |

- | Friday 18 April 2014 09:30 - 10:30 | + | |09:30 - 10:30|Alex Simpson|Semantics of programming languages with effects 5| |

- | Alex Simpson "Semantics of programming languages with effects" 5 | + | |//Coffee Break//||| |

- | Friday 18 April 2014 10:30 - 11:00 | + | |11:00 - 12:00|Alex Simpson|Semantics of programming languages with effects 6| |

- | Coffee Break | + | |//Lunch//||| |

- | Friday 18 April 2014 11:00 - 12:00 | + | |14:00 - 15:00|Amal Ahmed|Syntax and semantics of low level languages 5| |

- | Alex Simpson "Semantics of programming languages with effects" 6 | + | |//Coffee Break//||| |

- | Friday 18 April 2014 12:00 - 14:00 | + | |15:30 - 16:30|Amal Ahmed|Syntax and semantics of low level languages 6| |

- | Lunch | + | |//Dinner (CIRM Marseille)//||| |

- | Friday 18 April 2014 14:00 - 15:00 | + | ===== Talks ===== |

- | Amal Ahmed "Syntax and semantics of low level languages" 5 | + | ==== First week ==== |

- | Friday 18 April 2014 15:00 - 15:30 | + | |

- | Coffee Break | + | |

- | Friday 18 April 2014 15:30 - 16:30 | + | |

- | Amal Ahmed "Syntax and semantics of low level languages" 6 | + | |

- | Friday 18 April 2014 19:30 - 21:00 | + | |

- | Dinner (CIRM Marseille) | + | |

- | + | ||

- | === Saturday 19 April 2014 | + | |

- | Saturday 19 April 2014 12:00 - 13:00 | + | |

- | Lunch (CIRM Marseille) | + | |

- | + | ||

- | ==== Week 1 ==== | + | |

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, 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 **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. | ||

Line 181: | Line 122: | ||

* 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. |

Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.