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 locality 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 names. 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 representation independence 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 monadic 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.