TY - JOUR
T1 - Extending the lambda-calculus with unbind and rebind
AU - Dezani-Ciancaglini, Mariangiola
AU - Giannini, Paola
AU - Zucca, Elena
PY - 2011/1
Y1 - 2011/1
N2 - 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.
AB - 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.
KW - Lambda calculus
KW - Rebinding
KW - Static and dynamic scoping
KW - Type systems
UR - http://www.scopus.com/inward/record.url?scp=84863509049&partnerID=8YFLogxK
U2 - 10.1051/ita/2011008
DO - 10.1051/ita/2011008
M3 - Article
SN - 0988-3754
VL - 45
SP - 143
EP - 162
JO - RAIRO - Theoretical Informatics and Applications
JF - RAIRO - Theoretical Informatics and Applications
IS - 1
ER -