Extending the lambda-calculus with unbind and rebind. (English) Zbl 1220.68045

Summary: We extend the simply typed \(\lambda \)-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.


68N18 Functional programming and lambda calculus
Full Text: DOI EuDML Link


[1] D. Ancona, S. Fagorzi and E. Zucca, A parametric calculus for mobile open code. Electronic Notes in Theoretical Computer Science192 (2008) 3-22. · Zbl 1277.68158
[2] 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. · Zbl 1315.68047
[3] L. Dami, A lambda-calculus for dynamic binding. Theoret. Comput. Sci.192 (1997) 201-231. Zbl0895.68015 · Zbl 0895.68015
[4] M. Dezani-Ciancaglini, P. Giannini and O. Nierstrasz, A calculus of evolving objects. Scientific Annals of Computer Science (2008) 63-98.
[5] 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. · Zbl 1220.68045
[6] O. Kiselyov, C.-C. Shan and A. Sabry, Delimited dynamic binding, in ICFP’06, ACM Press (2006), 26-37.
[7] L. Moreau, A syntactic theory of dynamic binding. Higher Order and Symbolic Computation11 (1998) 233-279. · Zbl 0934.68038
[8] 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. · Zbl 1125.68023
[9] W. Taha and T. Sheard, MetaML and multi-stage programming with explicit annotations. Theoret. Comput. Sci.248 (2000) 211-242. · Zbl 0949.68047
[10] É. Tanter, Beyond static and dynamic scope, in DLS’09. ACM Press (2009), 3-14.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.