Department of Computer Science and Technology

Technical reports

Dynamic rebinding for marshalling and update, with destruct-time λ

Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough

February 2004, 85 pages


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 λ-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 λ-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of λ-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 λ-update calculus with simple primitives to provide type-safe updating of running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

Full text

PDF (0.7 MB)

BibTeX record

  author =	 {Bierman, Gavin and Hicks, Michael and Sewell, Peter and
          	  Stoyle, Gareth and Wansbrough, Keith},
  title = 	 {{Dynamic rebinding for marshalling and update, with
         	   destruct-time $\lambda$}},
  year = 	 2004,
  month = 	 feb,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-568}