Lambda the Ultimate

Polymorphic Delimited Contiunations by Kenichi Asai and Yukiyoshi Kameyama, in the 5^th ASIAN Symposium on Programming Languages and Systems (2007).

This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations.

Now, the real reason that I post this is because of Oleg's ShiftResetGenuine, which implements polymorphic delimited continuations in Haskell, and primarily cites this paper as well as Robert Atkey's Parameterized Notions of Computation. So if you find this paper challenging to read, Oleg provides you with a concrete playground in which to experiment.

It's also notable that Matthieu Sozeau has GenuineShiftReset available, which is a Coq version of Oleg's code.