Skip to Main content Skip to Navigation
Journal articles

Bisimulations for Delimited-Control Operators

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.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-02307669
Contributor : Sergueï Lenglet <>
Submitted on : Monday, October 7, 2019 - 5:54:38 PM
Last modification on : Saturday, November 21, 2020 - 9:54:03 AM

Links full text

Identifiers

Collections

Citation

Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Bisimulations for Delimited-Control Operators. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, 15 (2), pp.18:1-18:57. ⟨10.23638/LMCS-15(2:18)2019⟩. ⟨hal-02307669⟩

Share

Metrics

Record views

69