Transition systems over games

ABSTRACT. This paper describes a framework for game semantics combining operational and denotational accounts. The operational part is given by a transition system in which the set of permitted actions changes over time, as described by the rules of a game. The denotational part is given by a ``transfer'' between games, which describes a way of operating on strategies. The agreement between the two is given by a relation called a ``stepped bisimulation''. The framework is illustrated by an example of substitution within a lambda-calculus.