This dissertation presents a study of functional programming languages with first-class delimited continuations. We focus mainly on theoretical and practical aspects of Danvy and Filinski’s hierarchy of static delimited-control operators shiftn and resetn, and of Felleisen’s dynamic delimited-control operators control and prompt. Our study uses the traditional means of specifying semantics of functional languages: higher-order interpreters and abstract machines. We therefore first investigate the essence of interpreters and abstract machines, and we present a systematic and constructive derivation method connecting them. The functional correspondence we propose relates known higher-order interpreters and abstract machines that were invented independently and were believed to be disconnected, and it allows to construct new ones. We treat functional and logic programming languages.

Having established our enabling technology, we turn to the main topic of this dissertation, ie, delimited continuations. We use continuation-passing style (CPS) as a guide to build an operational foundation for static delimited continuations in the CPS hierarchy: We derive an abstract machine and a reduction semantics for the λ-calculus extended with control operators shiftn and resetn. We also characterize in what sense dynamic-control operators are incompatible with traditional CPS. Additionally, we present new applications of delimited continuations in the CPS hierarchy. We then formalize and prove the folklore theorem that the static delimitedcontrol operators shift and reset can be simulated in terms of the dynamic delimited-control operators control and prompt. We also show that breadth-first traversal exploits the difference between shift and control. For the last 15 years, this difference has been repeatedly mentioned in the literature but it has only been illustrated with one-line toy examples. Breadth-first traversal fills this vacuum. We point out how static delimited continuations naturally give rise to the notion of control stack whereas dynamic delimited continuations can account for a notion of ‘control queue.’Finally, we design a ‘dynamic continuation-passing style’for dynamic delimited continuations. This dynamic CPS underlies a new abstract machine, an interpreter, a CPS transformation, and a computational monad for dynamic delimited continuations. We also present a new simulation of dynamic delimited continuations in terms of static ones.