The Community for Technology Leaders
Logic in Computer Science, Symposium on (2004)
Turku, Finland
July 13, 2004 to July 17, 2004
ISSN: 1043-6871
ISBN: 0-7695-2192-4
pp: 150-159
S. Abramsky , Oxford University
C.-H. L. Ong , Oxford University
D. R. Ghica , Oxford University
I. D. B. Stark , Edinburgh University
A. S. Murawski , Oxford University
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.
S. Abramsky, C.-H. L. Ong, D. R. Ghica, I. D. B. Stark, A. S. Murawski, "Nominal Games and Full Abstraction for the Nu-Calculus", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 150-159, 2004, doi:10.1109/LICS.2004.1319609
88 ms
(Ver 3.3 (11022016))