Séminaire, 12 mai 2016

Programme

10:30 – 12:00

Andrzej Murawski (Warwick University (UK))

Invited talk: Contextual approximation and higher-order procedures

We investigate the complexity of deciding contextual approximation (refinement) in finitary Idealized Algol, a prototypical language combining higher-order types with state. Earlier work in the area established the borderline between decidable and undecidable cases, and focussed on the complexity of deciding approximation between terms in normal form.

In contrast, in this paper we set out to quantify the impact of locally declared higher-order procedures on the complexity of establishing contextual approximation in the decidable scenarios. We show that the obvious decision procedure based on exhaustive beta-reduction can be beaten. Further, by classifying redexes by levels, we give tight bounds on the complexity of contextual approximation for terms that may contain redexes up to level k, namely, (k-1)-EXPSPACE-completeness.

Interestingly, the bound is obtained by selective beta-reduction: redexes from level 3 onwards can be fired without losing optimality, whereas redexes of level up to 2 are handled by a dedicated decision procedure based on game semantics and a variant of pushdown automata.

This is joint work with Ranko Lazic, presented at FoSSaCS 2016.

14:00 – 15:00

Simon Castellan (ENS Lyon)

Invited talk: The parallel intensionally fully abstract model for PCF

In this talk, we introduce a new way to compose innocent strategies (a semantic representation of normal terms of PCF) based on the work of Rideau-Winskel on concurrent games on event structures.

This new framework can also deal with a notion of "concurrent innocent strategies" that can be composed and still form a model of PCF where term evaluation features some parallelism. We show that, similarly to Hyland and Ong's original construction, the quotient of this model by contextual equivalence is fully abstract for PCF, conveying the intuition that PCF terms cannot observe the fact that they are evaluated in parallel or sequentially.

15:30 – 16:30

Tom Hirschowitz (Univ. Savoie Mont Blanc)

Invited talk: A sheaf-based approach to concurrent innocent strategies

This talk is an introduction to a sheaf-based approach to programming language semantics, developed since 2011 with Clovis Eberhart, Damien Pous and Thomas Seiller.

In a sense, the intersection of presheaf models and innocent game semantics is boolean presheaves on traces with the prefix ordering. In the same sense, our approach takes the union. It proceeds in two main layers.

The high-level layer essentially implements the idea that if one considers a rich enough notion of play, then the innocence of game semantics may be encoded as a sheaf condition. Richness here means sufficient sensitivity to causality information. The sheaf condition means that any play is covered by its views, for the topology-like sense of `covered' provided by Grothendieck topologies. We will sketch our general notion of playground and how each playground gives rise to a family of categories of innocent strategies.

The low-level layer is concerned with the construction of relevant playgrounds. In the first installments of our approach, we constructed playgrounds for CCS and the pi-calculus, by hand. In recent work with Clovis, we started to generalise the process. I will illustrate this by constructing a candidate playground for the original HO games, which will turn out to also illustrate an important limitation of the current approach.

• slides