Bisimulations for Delimited-Control Operators

TL;DR

This paper develops a comprehensive behavioral theory for an untyped lambda calculus with delimited-control operators, introducing various bisimilarities to characterize contextual equivalence.

Contribution

It defines and compares multiple bisimilarities for the calculus, providing a unified framework and insights into their relative strengths and weaknesses.

Findings

Applicative, normal-form, and environmental bisimilarities are characterized.

The framework effectively captures behavioral equivalences for delimited-control operators.

Extensions to other control operators are discussed.

Abstract

We present a comprehensive study of the behavioral theory of an untyped $\lambda$-calculus extended with the delimited-control operators shift and reset. To that end, we define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We consider different styles of bisimilarities (namely applicative, normal-form, and environmental) within a unifying framework, 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.