some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 6, ISSUE 1, PAPER 2


A Graph Model for Imperative Computation

©Guy Andr McCusker, University of Bath

Abstract
Scott's graph model is a lambda-algebra based on the observation thatcontinuous endofunctions on the lattice of sets of natural numbers can berepresented via their graphs. A graph is a relation mapping finite sets ofinput values to output values. We consider a similar model based on relations whose input values are finitesequences rather than sets. This alteration means that we are taking intoaccount the order in which observations are made. This new notion of graphgives rise to a model of affine lambda-calculus that admits an interpretationof imperative constructs including variable assignment, dereferencing andallocation. Extending this untyped model, we construct a category that provides a modelof typed higher-order imperative computation with an affine type system. Anappropriate language of this kind is Reynolds's Syntactic Control ofInterference. Our model turns out to be fully abstract for this language. At aconcrete level, it is the same as Reddy's object spaces model, which was thefirst "state-free" model of a higher-order imperative programming language andan important precursor of games models. The graph model can therefore be seenas a universal domain for Reddy's model.

Publication date: January 12, 2010

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-6(1:2)2010

Hit Counts: 4286

Creative Commons