Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Bisimulations for Delimited-Control Operators

Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [78 references]  Display  Hide  Download
Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Wednesday, September 20, 2017 - 12:17:37 PM
Last modification on : Wednesday, October 26, 2022 - 8:14:16 AM


Files produced by the author(s)


  • HAL Id : hal-01207112, version 3


Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Bisimulations for Delimited-Control Operators. [Research Report] RR-9096, Inria Nancy - Grand Est. 2017. ⟨hal-01207112v3⟩



Record views


Files downloads