PhD Dissertation, University of Cambridge, December 1994. Also available as Technical Report No. 363, University of Cambridge Computer Laboratory.

Fetch thesis (PDF, 764k). Go to other papers, talks or my home page.

Many functional programming languages rely on the elimination of `impure'
features: assignment to variables, exceptions and even input/output. But some
of these are genuinely useful, and it is of real interest to establish how
they can be reintroducted in a controlled way. This dissertation looks in
detail at one example of this: the addition to a functional language of
dynamically generated *names*. Names are created fresh, they can be
compared with each other and passed around, but that is all. As a very basic
example of *state*, they capture the graduation between private and
public, local and global, by their interaction with higher-order functions.

The vehicle for this study is the *nu-calculus*, an extension of the
simply-typed lambda-calculus. The nu-calculus is equivalent to a certain
fragment of Standard 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.

Various operational and denotational methods for reasoning about the nu-calculus are developed. These include a computational metalanguage in the style of Moggi, which distinguishes in the type system between values and computations. This leads to categorical models that use a strong monad, and examples are devised based on functor categories.

The idea of *logical relations* is used to derive powerful reasoning
methods that capture some of the distinction between private and public names.
These techniques are shown to be complete for establishing contextual
equivalence between first-order expressions; they are also used to construct a
correspondingly abstract categorical model.

All the work with the nu-calculus extends cleanly to
*Reduced ML*, a larger language that introduces integer
*references*: mutable storage cells that are dynamically allocated.
It turns out that the step up is quite simple, and both the computational
metalanguage and the sample categorical models can be reused.

@PhdThesis{stark:namhof, author = {Ian Stark}, title = {Names and Higher-Order Functions}, school = {University of Cambridge}, year = 1994, month = dec, note = {Also available as Technical Report~363, University of Cambridge Computer Laboratory}, url = {http://www.inf.ed.ac.uk/~stark/namhof.html}, pdf = {http://www.inf.ed.ac.uk/~stark/namhof.pdf} }

This research was supported by UK SERC studentship 91307943.