BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Relating Two Semantics of Locally Scoped Names - Steffen Lösch (U
 niversity of Cambridge)
DTSTART:20110830T120000Z
DTEND:20110830T130000Z
UID:TALK32485@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Abstract: The operational semantics of programming constructs 
 involving locally scoped names typically makes use of stateful dynamic all
 ocation: a set of currently-used names forms part of the state and upon en
 tering a scope the set is augmented by a new name bound to the scoped iden
 tifier. More abstractly\, one can see this as a transformation of local sc
 opes by expanding them outward to an implicit top-level. By contrast\, in 
 a neglected paper from 1994\, Odersky gave a stateless lambda calculus wit
 h locally scoped names whose dynamics contracts scopes inward. The propert
 ies of ‘Odersky-style’ local names are quite different from dynamicall
 y allocated ones and it has not been clear\, until now\, what is the expre
 ssive power of Odersky’s notion. In this talk I will show that in fact i
 t provides a direct semantics of locally scoped names from which the more 
 familiar dynamic allocation semantics can be obtained by continuation-pass
 ing style (CPS) translation. More precisely\, I will introduce a typed lam
 bda calculus with dynamically allocated names (the Pitts-Stark ν-calculus
 ) as well as Odersky’s λν-calculus\, and show that there is a CPS tran
 slation of one into the other which is computationally adequate with respe
 ct 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) wit
 h Andy Pitts that will be published at CSL 2011.
LOCATION:Room SS03\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR