misc‎ > ‎

Algorithmic Nominal Game Semantics - June 2011


In their paper "Algorithmic Nominal Game Semantics", which appeared at ESOP (the 19th European Symposium on Programming) in March, Andrzej Murawski and Nikos Tzevelekos presented an algorithmic characterisation of a fragment of the ML language with numerical references. Their construction comes as a culmination of a three-year long collaboration and capitalises on major achievements of the last years in semantics of programs with dynamic generation of resources, and in particular on nominal game semantics and fresh-register automata.

Devising precise descriptions of higher-order programs with dynamic generation of resources is a daunting task, especially if one is interested in focussing just on observable behaviours. The reasons for this complication are due to the fact that dynamic resources combined with
  higher-order functions give rise to issues of privacy and data flow which cannot be resolved by standard analyses. A major breakthrough in this direction has been made recently with the introduction of nominal game semantics, a strand of the well-established theory of game semantics which addresses generative dynamic behaviours.

Andrzej and Nikos have been instrumental, not only in developing the theory, but also applying it towards giving algorithmic representations of its models. In a paper which appeared in FOSSACS (the 12th International Conference on Foundations of Software Science and Computation Structures) in 2009, they introduced a game model of Reduced ML, a fragment of ML with integer variables. Their model was the first such to provide an explicit characterisation of observable program behaviour – and it did so in a compositional denotational
  manner. Moreover, the explicitness of the description allowed for algorithmic representations of the model, by means of abstract machines.

Primitive such machines for dynamic resource generation, called fresh-register automata, had been recently introduced by Nikos in a paper which appeared in POPL (the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages) earlier this year. Andrzej and Nikos further extended these machines to capture game semantics. They were thus able to represent their model of a non-trivial fragment of Reduced ML and thus prove decidability of program equivalence. This is the first such result in languages with dynamic generative features and paves the way for algorithmic descriptions of other languages of this kind, including fragments of Java or C#.