Bisimulations for Delimited-Control Operators

04/23/2018
by   Dariusz Biernacki, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset