University of Cambridge > > Semantics Lunch (Computer Laboratory) > Relating Two Semantics of Locally Scoped Names

Relating Two Semantics of Locally Scoped Names

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

Note unusual day, time and place: this will be in the ARG lunch slot

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 ( with Andy Pitts that will be published at CSL 2011 .

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity