Proofs and programs (13 – 17 February)

Schedule

Monday 13

11:00 - 12:30
Lecture Hugo Herbelin (INRIA, Paris, France) Classical logic and control operators
14:00 - 15:00
Invited talk Peter Dybjer (Chalmers University) Tests, games, and Martin-Löf's meaning explanations for intuitionistic type theory.
15:00 - 16:00
Invited talk Ulrich Berger (Swansea, UK) Extracting concrete programs from abstract mathematics
16:30 - 17:15
Contributed talk Shin-ya Katsumata (RIMS, Kyoto, Japan) A Generic Soundness Result for Effect Systems

Tuesday 14

9:00 - 10:30
Lecture Guy McCusker (Bath, UK) Strategies and programs
11:00 - 12:30
Lecture Alexandre Miquel (ENS Lyon, France) Classical realizability — Introduction to classical realizability
14:00 - 15:00
Invited talk Thomas Streicher (Darmdstadt, Germany) The Classical Realizability Tripos and Topos
15:30 - 16:15
Contributed talk Mauricio Guillermo Specifying arithmetical formulae in classical realizability
16:15 - 17:00
Contributed talk Guilhem Jaber Forcing the Calculus of Construction to get Generalized Inductive Types

Wednesday 15

9:00 - 10:30
Lecture Guy McCusker (Bath, UK) Strategies and programs
11:00 - 12:30
Lecture Alexandre Miquel (ENS Lyon, France) Classical realizability — Models induced by classical realizability

Thursday 16

9:00 - 10:30
Lecture Gordon Plotkin (Edinburgh, UK) Introduction to the algebraic theory of effects
11:00 - 12:30
Lecture Hugo Herbelin (INRIA, Paris, France) Proving with delimited control
14:00 - 15:00
Invited talk Jaap van Oosten (Utrecht, Netherlands) Local Operators in the Effective Topos
15:30 - 16:15
Contributed talk Pierre Boutillier Delimited Control and Continuation Passing Style in Pure Type Systems
16:15 - 17:00
Contributed talk Jonas Frey Basic relational objects and partial combinatory algebras

Friday 17

9:00 - 10:30
Lecture Gordon Plotkin (Edinburgh, UK) Introduction to the algebraic theory of effects
11:00 - 12:30
Lecture Hugo Herbelin (INRIA, Paris, France) On the use of side effects in logic
14:00 - 15:00
Invited talk Paul-André Melliès (CNRS, Paris, France) Tensorial logic with algebraic effects
15:00 - 15:45
Contributed talk Paul Blain Levy (University of Birmingham) Call-by-push-value: the fine-grained structure of call-by-value and call-by-name