Abstract

Abstract: The operational semantics of programming constructs involving locally scoped names typically makes use of stateful dynamic allocation: a set of currently-used names forms part of the state and upon entering a scope the set is augmented by a new name bound to the scoped identifier. More abstractly, one can see this as a transformation of local scopes by expanding them outward to an implicit top-level. By contrast, in a neglected paper from 1994, Odersky gave a stateless lambda calculus with locally scoped names whose dynamics contracts scopes inward. The properties of ‘Odersky-style’ local names are quite different from dynamically allocated ones and it has not been clear, until now, what is the expressive power of Odersky’s notion. In this talk I will show that in fact it provides a direct semantics of locally scoped names from which the more familiar dynamic allocation semantics can be obtained by continuation-passing style (CPS) translation. More precisely, I will introduce a typed lambda calculus with dynamically allocated names (the Pitts-Stark ν-calculus) as well as Odersky’s λν-calculus, and show that there is a CPS translation of one into the other which is computationally adequate with respect to observational equivalence in the two calculi. The talk is based on a joint paper (http://www.cl.cam.ac.uk/~amp12/papers/reltsl/reltsl.pdf) with Andy Pitts that will be published at CSL 2011 .