Bisimulations for Delimited-Control Operators

We propose a survey of the behavioral theory of an untyped lambda-calculus extended with the delimited-control operators shift and reset. We define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We study different styles of bisimilarities (namely applicative, normal form, and environmental), and we give several examples to illustrate their respective strengths and weaknesses. We also discuss how to extend this work to other delimited-control operators