Abstract

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.