Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

This is an old revision of the document!


PhD school at CIRM

Dates and location

The school covers two full weeks, from Monday April 7 (morning) till Friday April 18 (noon) 2014, and will be held at CIRM in Luminy, near Marseille, France.

Registration

Please register here if you are interested in participating.

Programme

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.

Monday 07 April 2014
09:30 - 10:30Thierry CoquandConstructive mathematics and homotopy type theory 1
Coffee Break
11:00 - 12:00Thierry CoquandConstructive mathematics and homotopy type theory 2
Lunch
14:00 - 15:00Assia MahboubiFormalization of mathematics in proof assistants 1
Coffee Break
15:30 - 16:30Assia MahboubiFormalization of mathematics in proof assistants 2
17:00 - 18:00Working groups and exercises
Dinner
Tuesday 08 April 2014
09:30 - 10:30Thierry CoquandConstructive mathematics and homotopy type theory 3
Coffee Break
11:00 - 12:00Thierry CoquandConstructive mathematics and homotopy type theory 4
Lunch
14:00 - 15:00Assia MahboubiFormalization of mathematics in proof assistants 3
Coffee Break
15:30 - 16:30Assia MahboubiFormalization of mathematics in proof assistants 4
17:00 - 18:00Working groups and exercises
Dinner
Wednesday 09 April 2014
09:30 - 10:30Alexandre MiquelComputational interpretation of proofs and realizability 1
Coffee Break
11:00 - 12:00Alexandre MiquelComputational interpretation of proofs and realizability 2
Lunch and free afternoon
Thursday 10 April 2014
09:30 - 10:30Alexandre MiquelComputational interpretation of proofs and realizability 3
Coffee Break
11:00 - 12:00Alexandre MiquelComputational interpretation of proofs and realizability 4
Lunch
14:00 - 15:00Assia MahboubiFormalization of mathematics in proof assistants 5
Coffee Break
15:30 - 16:30Assia MahboubiFormalization of mathematics in proof assistants 6
17:00 - 18:00Working groups and exercises
Social dinner (bouillabaisse) (CIRM Marseille)

=== Friday 11 April 2014 Friday 11 April 2014 09:30 - 10:30 Thierry Coquand “Constructive mathematics and homotopy type theory” 5 Friday 11 April 2014 10:30 - 11:00 Coffee Break Friday 11 April 2014 11:00 - 12:00 Thierry Coquand “Constructive mathematics and homotopy type theory” 6 Friday 11 April 2014 12:00 - 14:00 Lunch 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 12:00 - 13:00 Lunch (CIRM Marseille)

=== Monday 14 April 2014 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 Monday 14 April 2014 11:00 - 12:00 Pierre-Louis Curien “Linear logic, game semantics and environment = machines” 2 Monday 14 April 2014 12:00 - 14:00 Lunch Monday 14 April 2014 14:00 - 15:00 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 09:30 - 10:30 Pierre-Louis Curien “Linear logic, game semantics and environment = machines” 3 Tuesday 15 April 2014 10:30 - 11:00 Coffee Break Tuesday 15 April 2014 11:00 - 12:00 Pierre-Louis Curien “Linear logic, game semantics and environment = machines” 4 Tuesday 15 April 2014 12:00 - 14:00 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 09:30 - 10:30 Amal Ahmed “Syntax and semantics of low level languages” 1 Wednesday 16 April 2014 10:30 - 11:00 Coffee Break 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 09:30 - 10:30 Pierre-Louis Curien “Linear logic, game semantics and environment = machines” 5 Thursday 17 April 2014 10:30 - 11:00 Coffee Break Thursday 17 April 2014 11:00 - 12:00 Pierre-Louis Curien “Linear logic, game semantics and environment = machines” 6 Thursday 17 April 2014 12:00 - 14:00 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 09:30 - 10:30 Alex Simpson “Semantics of programming languages with effects” 5 Friday 18 April 2014 10:30 - 11:00 Coffee Break Friday 18 April 2014 11:00 - 12:00 Alex Simpson “Semantics of programming languages with effects” 6 Friday 18 April 2014 12:00 - 14:00 Lunch Friday 18 April 2014 14:00 - 15:00 Amal Ahmed “Syntax and semantics of low level languages” 5 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.

  • 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 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 (Universidad de la República, Montevideo): 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.

Week 2

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 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 effects and monads, metalanaguages for effects, algebraic theory of effects, continuations, presheaf models of local store, observations and modalities.
  • Discussion sessions as well as practical sessions on the computer.

Organizers

  • Pierre-Louis Curien, directeur de recherche CNRS, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot
  • Hugo Herbelin, directeur de recherche INRIA, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot
  • Paul-André Melliès, chargé de recherche CNRS, Laboratoire Preuves, Programmes, Systèmes (PPS), Université Paris Diderot
cirm.1394200498.txt.gz · Last modified: 2014/03/07 14:54 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