The purpose of this workshop is to survey the state of the art of
sequential algorithms, and to explore connections, whether well
established or more speculative, with other concepts
in the field of logic in computer science — game semantics, models of
dependent types and the Dialectica interpretation.
We want the workshop to offer an open and friendly atmosphere,
encouraging informal but informed discussions.
Programme
Thursday 9 June:
- 10:00-11:00,
Pierre-Louis Curien:
- Sequential algorithms, from the source
- 11:00-11:30:
- short break
- 11:30-12:30,
Pierre Clairambault:
- Sequential algorithms and games, take 1 (tentative title)
- 12:30-14:00:
- lunch
- 14:00-15:00, Paul-André Melliès
- Sequential algorithms and games, take 2 (tentative title)
- 15:00-16:30:
- break and discussions
- 16:30-17:30,
Pierre-Marie Pédrot:
- Dialectica for dummies (tentative title)
- 17:30-???:
- discussions, dinner, etc.
Friday 10 June:
- 9:30-10:30,
Sean Moss:
- A sheaf model of sequentiality
-
Abstract: Subsequent to approaches using game semantics, a fully
abstract model of PCF based on logical relat ions was given by
O'Hearn and Riecke. Their construction gives an interpretation in
a well-pointed cartesian closed category without quotienting an
intermediate intensional model. On the other hand, its description
requires an unwieldy collection of 'arities' for logical
relations. I will explain how this technique can be adapted to
directly give a model of Synthetic Domain Theory, i.e. a topo s
equipped with a notion of partial morphism such that the
'canonical' interpretation of call-by-va lue PCF (interpreting the
base type as the actual natural numbers object) is fully abstract.
I will make use of a general framework for using concrete sheaves
to add higher-order types and recursion to a first-order
structure. The talk is based on joint work with Cristina Matache
and Sam Staton.
- 10:30-11:30:
- break and discussions
- 11:30-12:30,
Valentin Blot:
- Extensional and intensional semantic universes: a denotational model of dependent types
- 12:30-???
- lunch and discussions
Venue
The meeting will take place at the CIRM,
in room S2 (next to the library of the CIRM).
Lunch will be offered to registered participants (up to a limited capacity).
Registration
Registration is closed.
Registration is free but mandatory, using the dedicated registration form, ASAP.
The firm deadline is Sunday 29 May.
Organization
If you have any question regarding the workshop,
please contact the local organizer.
Participants
- Victor Blanchi (ÉNS PSL & I2M, Aix-Marseille)
- Lison Blondeau (I2M+LIS, Aix-Marseille)
- Filippo Bonchi (Dipartimento di Informatica, Pisa)
- Valentin Blot (LMF, Paris-Saclay)
- Pierre Clairambault (LIS, Aix-Marseille)
- Raphaëlle Crubillé (LIS, Aix-Marseille)
- Pierre-Louis Curien (IRIF, Paris Cité)
- Simon Forest (I2M, Aix-Marseille)
- Samuel Gardelle (ÉNS Lyon & I2M, Aix-Marseille)
- Guilhem Jaber (LS2N, Nantes)
- Yves Lafont (I2M, Aix-Marseille)
- Paul-André Melliès (IRIF, Paris Cité)
- Étienne Miquey (I2M, Aix-Marseille)
- Sean Moss (Oxford)
- Alexey Muranov (I2M, Aix-Marseille)
- Pierre-Marie Pédrot (LS2N, Nantes)
- Laurent Regnier (I2M, Aix-Marseille)
- Lionel Vaux Auclair (I2M, Aix-Marseille)