Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction. Peter Sewell, Gareth Stoyle, Michael Hicks, Gavin Bierman, and Keith Wansbrough. Journal of Functional Programming (JFP), 18(4):437-502, July 2008. Appeared on-line October, 2007. Supercedes ICFP 2003 and USE 2003 papers.

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, for example when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics.

In this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply-typed call-by-value lambda-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a lambda-update calculus with simple primitives to provide type-safe updating of running code. We show how the ideas of this simple calculus extend to more real-world, module-level dynamic updating in the style of Erlang. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

[ .pdf ]

@ARTICLE{SewellSHBW07,
  AUTHOR = {Peter Sewell and Gareth Stoyle and Michael Hicks and Gavin Bierman and Keith Wansbrough},
  TITLE = {Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction},
  JOURNAL = {Journal of Functional Programming (JFP)},
  VOLUME = 18,
  NUMBER = 4,
  MONTH = JUL,
  PAGES = {437--502},
  YEAR = 2008,
  NOTE = {Appeared on-line October, 2007.  Supercedes ICFP 2003 and USE 2003 papers},
  OPTDOI = {doi: 10.1017/S0956796807006600}
}

This file has been generated by bibtex2html 1.69