Bisimulations for Delimited-Control Operators

Dariusz Biernacki (1) , Sergueï Lenglet (2) , Piotr Polesiuk (1)

1 UWr - University of Wrocław [Poland]
2 PAREO - Formal islands: foundations and applications

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.

Domaines: Langage de programmation [cs.PL]

Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Bisimulations for Delimited-Control Operators. 2017. ⟨hal-01207112v2⟩