Personal tools
You are here: Home Events Abstract Archives 1999 Towards a theory of bisimulation for local names.

Towards a theory of bisimulation for local names.

Julian Rathke School of Cognitive and Computing Sciences (COGS) University of Sussex 4pm Tuesday 4 May 1999 Room 2511, JCMB, King's Buildings

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.

Document Actions