Relating Two Semantics of Locally Scoped Names (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. We 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, we show
that there is a CPS translation of typed lambda calculus with
dynamically allocated names (the Pitts-Stark ν-calculus) into
Odersky's λν-calculus which is computationally adequate with
respect to observational equivalence in the two calculi.