Relating Two Semantics of Locally Scoped Names

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

• Steffen Lösch (University of Cambridge)
• Tuesday 30 August 2011, 13:00-14:00
• Room SS03, Computer Laboratory, William Gates Building.

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 (http://www.cl.cam.ac.uk/~amp12/papers/reltsl/reltsl.pdf) with Andy Pitts that will be published at CSL 2011 .

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

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room SS03, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.