McCusker, G. A. and Power, J., 2010. Modelling local variables: possible worlds and object spaces. Electronic Notes in Theoretical Computer Science, 265, pp. 389-402.
Local variables in imperative languages have been given denotational semantics in at least two fundamentally diﬀerent ways. One is by use of functor categories, focusing on the idea of possible worlds. The other might be termed event-based, exempliﬁed by Reddy’s object spaces and models based on game semantics. O’Hearn and Reddy have related the two approaches by giving functor category models whose worlds are ob ject spaces, then showing that their model is fully abstract for Idealised Algol programs up to order two. But the category of ob ject spaces is not small, and so in order to construct a functor category that is locally small, and hence Cartesian closed, they need to work with a restricted collection of ob ject spaces. This weakens the connection between the object spaces model and the functor-category model: the Yoneda embedding no longer provides a full embedding of the original category of object spaces into the functor-category. Moreoever the choice of the restricted collection of object spaces is ad hoc. In this paper, we reﬁne the approach by proving that the ﬁnite objects form a small dense subcategory of a simpliﬁed object-spaces model. The functor category over these ﬁnite objects is therefore locally small and Cartesian closed, and contains the object-spaces category as a full subcategory. All this work is necessarily enriched in Cpo. We further reﬁne their full abstraction result by showing that full abstraction fails at order three.
|Item Type ||Articles|
|Creators||McCusker, G. A.and Power, J.|
|Departments||Faculty of Science > Computer Science|
|Publisher Statement||density.pdf: Postprint version made available in accordance with Elsevier publisher policies. Article should always be cited as: McCusker, G., Power, J., 2010. Modelling local variables: possible worlds and object spaces. In: Selinger, P., ed. Proceedings, Twenty-sixth conference on the Mathematical Foundations of Programming Semantics, MFPS 2010. Elsevier.|
|Additional Information||Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)|
Actions (login required)