Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises. Typically it is provided only by ad-hoc mechanisms that lack clean semantics. In this paper we adopt a more foundational approach, showing how core dynamic rebinding mechanisms can be added to a CBV λ-calculus. To do so we first develop two refinements of the CBV reduction strategy with delayed instantiation, the redex-time and destruct-time semantics. Delayed instantiation ensures we obtain the most recent version of a definition following a rebinding. The destruct-time semantics gives the basis for a λ_marsh calculus that supports dynamic rebinding, with primitives to package values and marks to control which identifiers are dynamically rebound when they are unpackaged. We extend λ_marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed, and discuss the extent to which it can be statically typed. Finally, we use the destruct-time semantics also as a basis for a λ_update calculus with simple primitives to provide type-safe, dynamic updating of code. We thereby put a variety of real-world mechanisms on a common semantic foundation.

[ .pdf ]

@inproceedings{BiermanHSSW03,
  author = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough},
  title = {Dynamic Rebinding for Marshalling and Update with Destruct-time $\lambda$},
  booktitle = {Proceedings of the {ACM} International Conference on Functional Programming (ICFP)},
  month = {August},
  year = {2003},
  pages = {99--110},
  where = {Uppsala, Sweden}
}

This file was generated by bibtex2html 1.99.