License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2011.396
URN: urn:nbn:de:0030-drops-32454
Go to the corresponding LIPIcs Volume Portal

Lösch, Steffen ; Pitts, Andrew M.

Relating Two Semantics of Locally Scoped Names

32.pdf (0.4 MB)


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 nu-calculus) into Odersky's lambda-nu-calculus which is computationally adequate with respect to observational equivalence in the two calculi.

BibTeX - Entry

  author =	{Steffen L{\"o}sch and Andrew M. Pitts},
  title =	{{Relating Two Semantics of Locally Scoped Names}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{396--411},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-32454},
  doi =		{10.4230/LIPIcs.CSL.2011.396},
  annote =	{Keywords: local names, continuations, typed lambda-calculus, observational equivalence}

Keywords: local names, continuations, typed lambda-calculus, observational equivalence
Collection: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue Date: 2011
Date of publication: 31.08.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI