Hostname: page-component-cd9895bd7-gvvz8 Total loading time: 0 Render date: 2024-12-26T07:35:15.506Z Has data issue: false hasContentIssue false
  • English
  • Français

Extending the lambda-calculuswith unbind and rebind

Published online by Cambridge University Press:  15 March 2011

Mariangiola Dezani-Ciancaglini ,
Paola Giannini  and
Elena Zucca
Mariangiola Dezani-Ciancaglini
Affiliation:
Dip. di Informatica, Univ. di Torino, Italy; [email protected]
Paola Giannini
Affiliation:
Dip. di Informatica, Univ. del Piemonte Orientale, Italy.
Elena Zucca
Affiliation:
DISI, Univ. di Genova, Italy.
Get access

Abstract

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.

Keywords

Lambda calculustype systemsstatic and dynamic scopingrebinding
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 45 , Issue 1: ICTCS 09 , January 2011 , pp. 143 - 162
Copyright
© EDP Sciences, 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Ancona, D., Fagorzi, S. and Zucca, E., A parametric calculus for mobile open code. Electronic Notes in Theoretical Computer Science 192 (2008) 3–22. CrossRef
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.
Dami, L., A lambda-calculus for dynamic binding. Theoret. Comput. Sci. 192 (1997) 201–231. CrossRef
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. CrossRef
O. Kiselyov, C.-C. Shan and A. Sabry, Delimited dynamic binding, in ICFP'06, ACM Press (2006), 26–37.
Moreau, L., A syntactic theory of dynamic binding. Higher Order and Symbolic Computation 11 (1998) 233–279. CrossRef
Sewell, P., Leifer, J.J., Wansbrough, K., Allen-Williams, M., Nardelli, F.Z., Habouzit, P. and Vafeiadis, V., Acute: High-level programming language design for distributed computation: Design rationale and language definition. J. Funct. Prog. 17 (2007) 547–612. CrossRef
Taha, W. and Sheard, T., MetaML and multi-stage programming with explicit annotations. Theoret. Comput. Sci. 248 (2000) 211–242. CrossRef
É. Tanter, Beyond static and dynamic scope, in DLS'09. ACM Press (2009), 3–14.