### Abstract

Language | English |
---|---|

Pages | 389-402 |

Number of pages | 14 |

Journal | Electronic Notes in Theoretical Computer Science |

Volume | 265 |

DOIs | |

Status | Published - 6 Sep 2010 |

### Fingerprint

### Cite this

**Modelling local variables: possible worlds and object spaces.** / McCusker, Guy A; Power, John.

Research output: Contribution to journal › Article

*Electronic Notes in Theoretical Computer Science*, vol. 265, pp. 389-402. DOI: 10.1016/j.entcs.2010.08.023

}

TY - JOUR

T1 - Modelling local variables: possible worlds and object spaces

AU - McCusker,Guy A

AU - Power,John

N1 - Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)

PY - 2010/9/6

Y1 - 2010/9/6

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=77957923853&partnerID=8YFLogxK

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

U2 - 10.1016/j.entcs.2010.08.023

DO - 10.1016/j.entcs.2010.08.023

M3 - Article

VL - 265

SP - 389

EP - 402

JO - Electronic Notes in Theoretical Computer Science

T2 - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -