The research reported in this paper is concerned with the problem of
reasoning about properties of higher order functions involving state.
It is motivated by the desire to identify what, if any, are the
difficulties created purely by <i>locality</i> of state, independent
of other properties such as side-effects, exceptional termination and
non-termination due to recursion. We consider a simple language
(equivalent to a fragment of Standard ML) of typed, higher order
functions that can dynamically create fresh <i>names</i>. Names are
created with local scope, can be tested for equality and can be passed
around via function application, but that is all.

We demonstrate that despite the simplicity of the language and its
operational semantics, the observable properties of such functions can
be very subtle. Two methods are introduced for analyzing Morris-style
observational equivalence between expressions in the language. The
first method introduces a notion of `applicative' equivalence
incorporating a syntactic version of O'Hearn and Tennent's
relationally parametric functors and a version of <i>representation
independence</i> for local names. This applicative equivalence is
properly contained in the relation of observational equivalence, but
coincides with it for first order expressions (and is decidable
there). The second method develops a general, categorical framework
for computationally adequate models of the language, based on Moggi's
<i>monadic</i> approach to denotational semantics. We give examples
of models, one of which is fully abstract for first order expressions.
No fully abstract (concrete) model of the whole language is known.