Extending the lambda-calculus with unbind and rebind
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 45 (2011) no. 1, pp. 143-162

Voir la notice de l'article provenant de la source Numdam

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.

DOI : 10.1051/ita/2011008
Classification : 68N15, 68N18
Keywords: lambda calculus, type systems, static and dynamic scoping, rebinding
@article{ITA_2011__45_1_143_0,
     author = {Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Zucca, Elena},
     title = {Extending the lambda-calculus with unbind and rebind},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {143--162},
     publisher = {EDP-Sciences},
     volume = {45},
     number = {1},
     year = {2011},
     doi = {10.1051/ita/2011008},
     mrnumber = {2776858},
     zbl = {1220.68045},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.1051/ita/2011008/}
}
TY  - JOUR
AU  - Dezani-Ciancaglini, Mariangiola
AU  - Giannini, Paola
AU  - Zucca, Elena
TI  - Extending the lambda-calculus with unbind and rebind
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2011
SP  - 143
EP  - 162
VL  - 45
IS  - 1
PB  - EDP-Sciences
UR  - http://geodesic.mathdoc.fr/articles/10.1051/ita/2011008/
DO  - 10.1051/ita/2011008
LA  - en
ID  - ITA_2011__45_1_143_0
ER  - 
%0 Journal Article
%A Dezani-Ciancaglini, Mariangiola
%A Giannini, Paola
%A Zucca, Elena
%T Extending the lambda-calculus with unbind and rebind
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2011
%P 143-162
%V 45
%N 1
%I EDP-Sciences
%U http://geodesic.mathdoc.fr/articles/10.1051/ita/2011008/
%R 10.1051/ita/2011008
%G en
%F ITA_2011__45_1_143_0
Dezani-Ciancaglini, Mariangiola; Giannini, Paola; Zucca, Elena. Extending the lambda-calculus with unbind and rebind. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 45 (2011) no. 1, pp. 143-162. doi: 10.1051/ita/2011008

Cité par Sources :