Research

A graph model for imperative computation


Reference:

McCusker, G. A., 2010. A graph model for imperative computation. Logical Methods in Computer Science, 6 (1), Paper 2.

Related documents:

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

    Official URL:

    http://dx.doi.org/10.2168/LMCS-6(1:2)2010

    Related URLs:

    Abstract

    Scott's graph model is a lambda-algebra based on the observation that continuous endofunctions on the lattice of sets of natural numbers can be represented via their graphs. A graph is a relation mapping finite sets of input values to output values. We consider a similar model based on relations whose input values are finite sequences rather than sets. This alteration means that we are taking into account the order in which observations are made. This new notion of graph gives rise to a model of affine lambda-calculus that admits an interpretation of imperative constructs including variable assignment, dereferencing and allocation. Extending this untyped model, we construct a category that provides a model of typed higher-order imperative computation with an affine type system. An appropriate language of this kind is Reynolds's Syntactic Control of Interference. Our model turns out to be fully abstract for this language. At a concrete level, it is the same as Reddy's object spaces model, which was the first "state-free" model of a higher-order imperative programming language and an important precursor of games models. The graph model can therefore be seen as a universal domain for Reddy's model.

    Details

    Item Type Articles
    CreatorsMcCusker, G. A.
    DOI10.2168/LMCS-6(1:2)2010
    Related URLs
    URLURL Type
    http://arxiv.org/pdf/0910.5399.pdfFree Full-text
    DepartmentsFaculty of Science > Computer Science
    Publisher Statement0910.5399.pdf: This item is made available via a Creative Commons Attribution-NoDerivs 2.0 licence. The full citation for this item is: McCusker, G., 2010. A graph model for imperative computation. Logical Methods in Computer Science, 6 (1), 2.
    RefereedYes
    StatusPublished
    ID Code18531

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...