PhD Dissertation, University of Cambridge, December 1994. DOI: 10/cgnm. Also available as Technical Report 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, doi = {10/cgnm}, 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.