2013/09/16 by Dariusz Biernacki, Biernacki, Dariusz, Sergueï Lenglet +1
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #Petri Nets in System Modeling #Programming Languages (cs.PL) #cs.FL #cs.PL
paper · pdf · doi:10.48550/arxiv.1309.3919
Long version of the corresponding APLAS13 paper
arxiv created 2013/09/16 · openalex publication_date 2013/09/16 · arxiv updated 2013/09/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a theory of environmental bisimilarity for the delimited-control operators \it shift and \it reset. We consider two different notions of contextual equivalence: one that does not require the presence of a top-level control delimiter when executing tested terms, and another one, fully compatible with the original CPS semantics of shift and reset, that does. For each of them, we develop sound and complete environmental bisimilarities, and we discuss up-to techniques.