Title:  Nominal game semantics and automata

Abstract:  Names appear in computational scenarios where entities of specific kinds can be created at will and in such a manner that newly created entities are always fresh, i.e. distinct from any other created before. 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 semantic techniques for programs with names which have emerged in the last years. We will in particular focus on game semantics, a formalism that combines the extensional view of a program with a concrete operational description in terms of a game: a formal interaction between the program and its computational environment. "Nominal" games in particular have so far contributed fully abstract models for a variety of fragments of ML and an imperative fragment of Java. We moreover see how these models can be given algorithmic representations by means of automata operating on infinite alphabets.

Affiliation: School of Electronic Engineering and Computer Science, Queen Mary University of London

About Nikos Tzevelokos