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
Liste complète des métadonnées

Cited literature [78 references]  Display  Hide  Download

https://hal.inria.fr/hal-01207112
Contributor : Sergueï Lenglet <>
Submitted on : Wednesday, September 20, 2017 - 12:17:37 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM

File

RR-9096.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01207112, version 3

Citation

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

Share

Metrics

Record views

148

Files downloads

75