10.4230/LIPICS.CSL.2011.396
Lösch, Steffen
Steffen
Lösch
Pitts, Andrew M.
Andrew M.
Pitts
Relating Two Semantics of Locally Scoped Names
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
local names
continuations
typed lambda-calculus
observational equivalence
Bezem, Marc
Marc
Bezem
2011
2011-08-31
2011-08-31
2011-08-31
en
urn:nbn:de:0030-drops-32454
10.4230/LIPIcs.CSL.2011
978-3-939897-32-3
1868-8969
10.4230/LIPIcs.CSL.2011
LIPIcs, Volume 12, CSL 2011
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
2013
12
31
396
411
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Bezem, Marc
Marc
Bezem
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
12
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
16 pages
470133 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, pages 396-411