Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-12T12:04:14.305Z Has data issue: false hasContentIssue false

Extending the lambda-calculuswith unbind and rebind

Published online by Cambridge University Press:  15 March 2011

Mariangiola Dezani-Ciancaglini
Affiliation:
Dip. di Informatica, Univ. di Torino, Italy; dezani@di.unito.it
Paola Giannini
Affiliation:
Dip. di Informatica, Univ. del Piemonte Orientale, Italy.
Elena Zucca
Affiliation:
DISI, Univ. di Genova, Italy.

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We extend the simply typedλ-calculus with unbind and rebind primitiveconstructs. That is, a value can be a fragment of open code,which in order to be used should be explicitly rebound. Thismechanism nicely coexists with standard static binding. Themotivation is to provide an unifying foundation for mechanisms ofdynamic scoping, where the meaning of a name isdetermined at runtime, rebinding, such as dynamic updatingof 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 twoextensions which differ in the way type safety is guaranteed. Theformer relies on a combination of static and dynamic type checking.That is, rebind raises a dynamic error if for some variablethere 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 priceof more sophisticated types.

Information

Type
Research Article
Copyright
© EDP Sciences, 2011