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

Abstract

top
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.

How to cite

top

Dezani-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
  1. D. Ancona, S. Fagorzi and E. Zucca, A parametric calculus for mobile open code. Electronic Notes in Theoretical Computer Science192 (2008) 3–22.  
  2. G. Bierman, M.W. Hicks, P. Sewell, G. Stoyle and K. Wansbrough, Dynamic rebinding for marshalling and update, with destruct-time λ , in ICFP'03. ACM Press (2003), 99–110.  
  3. L. Dami, A lambda-calculus for dynamic binding. Theoret. Comput. Sci.192 (1997) 201–231.  
  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.  
  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.  
  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.  
  9. W. Taha and T. Sheard, MetaML and multi-stage programming with explicit annotations. Theoret. Comput. Sci.248 (2000) 211–242.  
  10. É. Tanter, Beyond static and dynamic scope, in DLS'09. ACM Press (2009), 3–14.  

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.