Delimited dynamic binding

Oleg Kiselyov, Chung Chieh Shan, Amr Sabry

Research output: Contribution to journalArticlepeer-review

14 Citations (Scopus)


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, OCaml, and Haskell. We extend DB + DC with mutable dynamic variables and a facility to obtain not only the latest binding of a dynamic variable but also older bindings. This facility provides for stack inspection and (more generally) folding over the execution context as an inductive data structure.

Original languageEnglish
Pages (from-to)26-37
Number of pages12
JournalACM SIGPLAN Notices
Issue number9
Publication statusPublished - 2006 Sept


  • Delimited continuations
  • Dynamic binding
  • Monads


Dive into the research topics of 'Delimited dynamic binding'. Together they form a unique fingerprint.

Cite this