Research

Modelling local variables: possible worlds and object spaces


Reference:

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:

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

    Official URL:

    http://dx.doi.org/10.1016/j.entcs.2010.08.023

    Abstract

    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.

    Details

    Item Type Articles
    CreatorsMcCusker, G. A.and Power, J.
    DOI10.1016/j.entcs.2010.08.023
    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.
    RefereedYes
    StatusPublished
    ID Code18530
    Additional InformationProceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...