# Extending the lambda-calculus with unbind and rebind

Mariangiola Dezani-Ciancaglini; Paola Giannini; Elena Zucca

RAIRO - Theoretical Informatics and Applications (2011)

- Volume: 45, Issue: 1, page 143-162
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topDezani-Ciancaglini, Mariangiola, Giannini, Paola, and Zucca, Elena. "Extending the lambda-calculus with unbind and rebind." RAIRO - Theoretical Informatics and Applications 45.1 (2011): 143-162. <http://eudml.org/doc/276339>.

@article{Dezani2011,

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.
},

author = {Dezani-Ciancaglini, Mariangiola, Giannini, Paola, Zucca, Elena},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Lambda calculus; type systems; static and dynamic scoping; rebinding; lambda calculus},

language = {eng},

month = {3},

number = {1},

pages = {143-162},

publisher = {EDP Sciences},

title = {Extending the lambda-calculus with unbind and rebind},

url = {http://eudml.org/doc/276339},

volume = {45},

year = {2011},

}

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

DA - 2011/3//

PB - EDP Sciences

VL - 45

IS - 1

SP - 143

EP - 162

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.

LA - eng

KW - Lambda calculus; type systems; static and dynamic scoping; rebinding; lambda calculus

UR - http://eudml.org/doc/276339

ER -

## References

top- D. Ancona, S. Fagorzi and E. Zucca, A parametric calculus for mobile open code. Electronic Notes in Theoretical Computer Science192 (2008) 3–22. Zbl1277.68158
- G. Bierman, M.W. Hicks, P. Sewell, G. Stoyle and K. Wansbrough, Dynamic rebinding for marshalling and update, with destruct-time $\lambda $, in ICFP'03. ACM Press (2003), 99–110. Zbl1315.68047
- L. Dami, A lambda-calculus for dynamic binding. Theoret. Comput. Sci.192 (1997) 201–231. Zbl0895.68015
- M. Dezani-Ciancaglini, P. Giannini and O. Nierstrasz, A calculus of evolving objects. Scientific Annals of Computer Science (2008) 63–98.
- M. Dezani-Ciancaglini, P. Giannini and E. Zucca, Intersection types for unbind and rebind, in ITRS'10. Electronic Proceedings in Theoretical Computer Science 45 (2010) 45–59. Zbl1220.68045
- O. Kiselyov, C.-C. Shan and A. Sabry, Delimited dynamic binding, in ICFP'06, ACM Press (2006), 26–37.
- L. Moreau, A syntactic theory of dynamic binding. Higher Order and Symbolic Computation11 (1998) 233–279. Zbl0934.68038
- P. Sewell, J.J. Leifer, K. Wansbrough, M. Allen-Williams, F.Z. Nardelli, P. Habouzit and V. Vafeiadis, Acute: High-level programming language design for distributed computation: Design rationale and language definition. J. Funct. Prog.17 (2007) 547–612. Zbl1125.68023
- W. Taha and T. Sheard, MetaML and multi-stage programming with explicit annotations. Theoret. Comput. Sci.248 (2000) 211–242. Zbl0949.68047
- É. Tanter, Beyond static and dynamic scope, in DLS'09. ACM Press (2009), 3–14.

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.