Delimited dynamic binding

Dynamic binding and delimited control are useful together in many settings, including Web applications, database cursors, and mobile code. We examine this pair of language features to show that the semantics of their interaction is ill-defined yet not expressive enough for these uses. We solve this open and subtle problem. We formalise a typed language DB+DC that combines a calculus DB of dynamic binding and a calculus DC of delimited control. We argue from theoretical and practical points of view that its semantics should be based on delimited dynamic binding: capturing a delimited continuation closes over part of the dynamic environment, rather than all or none of it; reinstating the captured continuation supplements the dynamic environment, rather than replacing or inheriting it. We introduce a type- and reduction-preserving translation from DB + DC to DC, which proves that delimited control macro-expresses dynamic binding. We use this translation to implement DB + DC in Scheme, OC...

• Type: Conference
• Year: 2006
• Where: ICFP
• Authors: Oleg Kiselyov, Chung-chieh Shan, Amr Sabry
• Keywords: Delimited Control, Delimited Dynamic Binding, ICFP 2006, Macro-expresses Dynamic Binding, Programming Languages