Ian Stark

Nominal Games and Full Abstraction for the Nu-Calculus

Samson Abramsky, Dan Ghica, Andrzej Murawski, Luke Ong and Ian Stark

In Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science, 13–17 July 2004, Turku, Finland, pages 150–159. IEEE Computer Society Press, 2004.

Fetch paper (PDF, 328k). Go to other papers, talks or home page.


We introduce nominal games for modelling programming languages with dynamically generated local names, as exemplified by Pitts and Stark's nu-calculus. Inspired by Pitts and Gabbay's recent work on nominal sets, we construct arenas and strategies in the world (or topos) of Fraenkel-Mostowski sets (or simply FM-sets). We fix an infinite set N of names to be the "atoms" of the FM-theory, and interpret the type ν of names as the flat arena whose move-set is N. This approach leads to a clean and precise treatment of fresh names and standard game constructions (such as plays, views, innocent strategies, etc.) that are considered invariant under renaming. The main result is the construction of the first fully-abstract model for the nu-calculus.

  author =       {Samson Abramsky and Dan Ghica and Andrzej Murawski and
                  Luke Ong and Ian Stark},
  title =        {Nominal Games and Full Abstraction for the
  booktitle =    {Proceedings of the Nineteenth Annual IEEE Symposium on
                  Logic in Computer Science},
  pages =        {150--159}, 
  year =         2004,
  publisher =    {IEEE Computer Society Press},
  url =          {http://www.inf.ed.ac.uk/~stark/nominalgames.html},
  pdf =          {http://www.inf.ed.ac.uk/~stark/nominalgames.pdf},
  doi =          {10.1109/LICS.2004.1319609}

Page last modified: Tuesday 5 August 2008