Towards a theory of bisimulation for local names

Pitts and Stark have proposed the nu-calculus as a language for the investigation of the interaction of unique name generation and higher-order functions. They developed a sound model based on logical relations but left completeness as an open problem. In this talk we attempt to tackle this problem by giving a complete model based on bisimulation for a labelled transition system semantics. We discover that the intuitive lts semantics we provide, whilst complete, are only found to be sound for the nu-calculus at first-order types. We go on to show that by extending the nu-calculus with a mild form of assignment we can obtain a fully abstract model. The analysis used to obtain this result illuminates some of the difficulty in finding a fully abstract model for the nu-calculus proper.

LS Home page or Talks in 1998/99