University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Transition systems over games

Transition systems over games

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jonathan Hayman.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity