Modelling local variables: possible worlds and object spaces


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.

Related documents:

PDF (density.pdf) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (221kB) | Preview

    Official URL:


    Local variables in imperative languages have been given denotational semantics in at least two fundamentally different ways. One is by use of functor categories, focusing on the idea of possible worlds. The other might be termed event-based, exemplified 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 refine the approach by proving that the finite objects form a small dense subcategory of a simplified object-spaces model. The functor category over these finite 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 refine their full abstraction result by showing that full abstraction fails at order three.


    Item Type Articles
    CreatorsMcCusker, G. A.and Power, J.
    DepartmentsFaculty of Science > Computer Science
    Publisher Statementdensity.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.
    ID Code18530
    Additional InformationProceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)


    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...