Comparing control constructs by typing double-barrelled CPS transforms

Hayo Thielecke

Research output: Contribution to journalArticlepeer-review

21 Citations (Scopus)


We investigate call-by-value continuation-passing style transforms that pass two continuations. Altering a single variable in the translation of λ-abstraction gives rise to different control operators: first-class continuations; dynamic control; and (depending on a further choice of a variable) either the return statement of C; or Landin's J-operator. In each case there is an associated simple typing. For those constructs that allow upward continuations, the typing is classical, for the others it remains intuitionistic, giving a clean distinction independent of syntactic details. Moreover, those constructs that make the typing classical in the source of the CPS transform break the linearity of continuation use in the target.
Original languageEnglish
Pages (from-to)141-160
JournalHigher-Order and Symbolic Computation
Issue number2-3
Publication statusPublished - 1 Sept 2002


Dive into the research topics of 'Comparing control constructs by typing double-barrelled CPS transforms'. Together they form a unique fingerprint.

Cite this