Nominal games and full abstraction for the nu-calculus

S Abramsky*, DR Ghica, AS Murawski, CHL Ong, IDB Stark

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 v 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.

Original languageEnglish
Title of host publicationLogic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages150-159
Number of pages10
ISBN (Print)0-7695-2192-4
DOIs
Publication statusPublished - 2004
Event19th Annual IEEE Symposium on Logic in Computer Science - Turku, Finland
Duration: 13 Jul 200417 Jul 2004

Conference

Conference19th Annual IEEE Symposium on Logic in Computer Science
CountryFinland
CityTurku
Period13/07/0417/07/04

Cite this