Towards a Theory of Bisimulation for Local Names

Pitts and Stark have proposed the -calculus as a language for investigating 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 paper, we develop a complete model based on bisimulation for a labelled transition system semantics. We show that bisimulation is complete, but not sound, for the -calculus. We also show that by adding assignment to the -calculus, bisimulation becomes sound and complete. The analysis used to obtain this result illuminates iculties involved in finding fully abstract models for -calculus proper.

• Type: Conference
• Year: 1999
• Where: LICS
• Authors: Alan Jeffrey, Julian Rathke
• Keywords: Automated Reasoning, Bisimulation, Complete Model, LICS 1999, Sound Model