Extending the lambda-calculus with unbind and rebind

Mariangiola Dezani-Ciancaglini, Paola Giannini, Elena Zucca

Risultato della ricerca: Contributo su rivistaArticolo in rivistapeer review

Abstract

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.

Lingua originaleInglese
pagine (da-a)143-162
Numero di pagine20
RivistaRAIRO - Theoretical Informatics and Applications
Volume45
Numero di pubblicazione1
DOI
Stato di pubblicazionePubblicato - gen 2011

Fingerprint

Entra nei temi di ricerca di 'Extending the lambda-calculus with unbind and rebind'. Insieme formano una fingerprint unica.

Cita questo