RAIRO-Theor. Inf. Appl.
Volume 45, Number 1, January-March 2011ICTCS 09
|Page(s)||143 - 162|
|Published online||15 March 2011|
Extending the lambda-calculus with unbind and rebind
Dip. di Informatica, Univ. di Torino, Italy; email@example.com
2 Dip. di Informatica, Univ. del Piemonte Orientale, Italy.
3 DISI, Univ. di Genova, Italy.
Accepted: 23 November 2010
We extend the simply typed λ-calculus with unbind and rebind primitive constructs. That is, a value can be a fragment of open code, which in order to be used should be explicitly rebound. This mechanism nicely coexists with standard static binding. The motivation is to provide an unifying foundation for mechanisms of dynamic scoping, where the meaning of a name is determined at runtime, rebinding, such as dynamic updating of resources and exchange of mobile code, and delegation, where an alternative action is taken if a binding is missing. Depending on the application scenario, we consider two extensions which differ in the way type safety is guaranteed. The former relies on a combination of static and dynamic type checking. That is, rebind raises a dynamic error if for some variable there is no replacing term or it has the wrong type. In the latter, this error is prevented by a purely static type system, at the price of more sophisticated types.
Mathematics Subject Classification: 68N15 / 68N18
Key words: Lambda calculus / type systems / static and dynamic scoping / rebinding
© EDP Sciences, 2011
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.