Ian Stark

Categorical Models for Local Names

LISP and Symbolic Computation, 9(1):77–107, February 1996.

Fetch a preprint of the article (PDF, 179k) or visit the publisher's page. Go to other papers, talks or my home page.

Abstract

This paper describes the construction of categorical models for the nu-calculus, a language that combines higher-order functions with dynamically created names. Names are created with local scope, they can be compared with each other and passed around through function application, but that is all.

The intent behind this language is to examine one aspect of the imperative character of Standard ML: the use of local state by dynamic creation of references. The nu-calculus is equivalent to a certain fragment of ML, omitting side effects, exceptions, datatypes and recursion. Even without all these features, the interaction of name creation with higher-order functions can be complex and subtle; it is particularly difficult to characterise the observable behaviour of expressions.

Categorical monads, in the style of Moggi, are used to build denotational models for the nu-calculus. An intermediate stage is the use of a computational metalanguage, which distinguishes in the type system between values and computations.

The general requirements for a categorical model are presented, and two specific examples described in detail. These provide a sound denotational semantics for the nu-calculus, and can be used to reason about observable equivalence in the language. In particular a model using logical relations is fully abstract for first-order expressions.

@Article{stark:catmln,
  author =       {Ian Stark},
  title =        {Categorical Models for Local Names},
  journal =      {{LISP} and Symbolic Computation},
  year =         1996,
  month =        feb,
  volume =       9,
  number =       1,
  pages =        {77--107},
  url =          {http://www.inf.ed.ac.uk/~stark/catmln.html},
  pdf =          {http://www.inf.ed.ac.uk/~stark/catmln.pdf}
}

This research was supported by UK SERC studentship 91307943 and CEC SCIENCE project PL910296.

Page last modified: Thursday 27 November 2008