Archive for the 'Nu-calculus' Category

Nominal games and full abstraction for the nu-calculus

By Samson Abramsky, Dan Ghica, Andrzej Murawski, Luke Ong and Ian Stark, from LICS 2004, available from Ian Stark’s website:

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.


Observable properties of higher-order functions that dynamically create local state: or, what’s new?

By Andrew Pitts and Iain Stark, from MFCS 1993, available from Iain Stark’s website:

The research reported in this paper is concerned with the problem of reasoning about properties of higher order functions involving state. It is motivated by the desire to identify what, if any, are the difficulties created purely by locality of state, independent of other properties such as side-effects, exceptional termination and non-termination due to recursion. We consider a simple language (equivalent to a fragment of Standard ML) of typed, higher order functions that can dynamically create fresh names; names are created with local scope, can be tested for equality and can be passed around via function application, but that is all. Despite the extreme simplicity of the language and its operational semantics, the observable properties of such functions are shown to be very subtle. A notion of `logical relation’ is introduced which incorporates a version of representation independence for local names. We show how to use it to establish observational equivalences. The method is shown to be complete (and decidable) for expressions of first order types, but incomplete at higher types.