Games with names

Nikos Tzevelekos

Names constitute a pervasive feature in programming languages. They appear in every computational scenario where entities of specific kinds can be created at will and, moreover, in such a manner that newly created entities are always fresh, i.e. distinct from any other created thus far. For example, references, objects and exceptions in languages like ML or Java can be seen as names. The behaviour of languages which feature names is in general very subtle due to issues of privacy, visibility and flow of names, and the ensuing notion of local state.

This talk is about formal reasoning techniques for programs with names which have emerged in the last years. We will focus on a specific such formalism, called game semantics, which models computation as a formal interaction (a game) between a program and its environment. We will moreover see how these models can be given algorithmic representations by means of newly introduced abstract machines, called Fresh-Register Automata, which operate on infinite alphabets of names.

The talk will begin with a gentle introduction of the basic notions, so no prior knowledge is required.