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

TitleDynamic rebinding for marshalling and update, with destruct-time ?
Publication TypeConference Papers
Year of Publication2003
AuthorsBierman G, Hicks MW, Sewell P, Stoyle G, Wansbrough K
Conference NameProceedings of the eighth ACM SIGPLAN international conference on Functional programming
Date Published2003///
Conference LocationNew York, NY, USA
ISBN Number1-58113-756-7
Keywordsdistributed programming, dynamic binding, dynamic update, lambda calculus, marshalling, programming languages, serialisation

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 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 ?marsh 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.