Date(s) : 04/12/2014 iCal
11 h 00 min - 12 h 30 min
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