Localisation

Adresses

Aix-Marseille Université
Institut de Mathématiques de Marseille (I2M) - UMR 7373
Site Saint-Charles : 3 place Victor Hugo, Case 19, 13331 Marseille Cedex 3
Site Luminy : Campus de Luminy - Case 907 - 13288 Marseille Cedex 9

Transition systems over games




Date(s) : 04/12/2014   iCal
11h00 - 12h30

We describe a framework for game semantics combining operational and denotational accounts. A game is a bipartite graph of “passive” and “active” positions, or a categorical variant with morphisms between positions.
The operational part of the framework is given by a labelled transition system in which each state sits in a particular position of the game. From a state in a passive position, transitions are labelled with a valid O-move from that position, and take us to a state in the updated position. Transitions from states in an active position are likewise labelled with a valid P-move, but silent transitions are allowed, which must take us to a state in the same position.
The denotational part is given by a “transfer” from one game to another, a kind of program that converts moves between the two games, giving an operation on strategies. The agreement between the two parts is given by a relation called a “stepped bisimulation”.
The framework is illustrated by an example of substitution within a lambda-calculus.
(Joint work with Sam Staton)

[http://www.cs.bham.ac.uk/~pbl/]

Catégories Pas de Catégories


Secured By miniOrange