Sequential algorithms and friends

9-10 June 2022
at the CIRM, Marseille

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