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. Despite the extreme
simplicity of the language and its operational semantics, the
observable properties of such functions are shown to be very subtle. A
notion of `logical relation' is introduced which incorporates a
version of <i>representation independence</i> for local names. We show
how to use it to establish observational equivalences. The method is
shown to be complete (and decidable) for expressions of first order
types, but incomplete at higher types.