Nominal Game Semantics

Abstract

Game Semantics arguably stands for one of the most successful techniques in denotational semantics, having provided not only proper denotational, accurate models for a large variety of programming languages, but also new semantical tools for program verification and validation. Most of all, over the last couple of decades, game semantics has contributed a novel understanding of computations, namely as functions with inner structure, the latter being described as interaction between two players—the Program and the Environment. On the other hand, Nominal Computation is a key theme within the Theory of Computation which has not been adressed semantically in a satisfactory manner. The significance of nominal computation is clearly depicted in the ubiquity of names in computational scenarios: names form the basis of many calculi of mobile processes; appear in network protocols and secure transactions; and are generally essential in programming for identifying variables, channels, threads, objects, codes, and many other sorts of name in disguise. This thesis examines nominal game semantics, that is, game semantics for nominal computation. Our starting point is the basic nominal language, the ν-calculus, which wemodel in a basic category of nominal games. The construction of nominal games is based on recent advances in game semantics, and also on the theory of Nominal Sets, which serves as a general foundation for reasoning about names. Our main focus is on languages extending the basic nominal language by use of names for general references and exceptions. These languages faithfully reflect the practice and reach the expressivity of programming languages such as ML; moreover, their full-abstraction problems had not been solved previously in a fully satisfactory manner. Such solutions we provide herein. We first devise abstract categoricalmodels for these languages, and then construct fully abstract models in nominal games.