Search

• < Previous
• 1
• Next >

---

An Operational Foundation for Delimited Continuations in the CPS Hierarchy

Malgorzata Biernacka ; Dariusz Biernacki ; Olivier Danvy.

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a&nbsp;[&hellip;]

---

Proving Soundness of Extensional Normal-Form Bisimilarities

Dariusz Biernacki ; Serguei Lenglet ; Piotr Polesiuk.

Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in $\lambda$-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation&nbsp;[&hellip;]

---

Bisimulations for Delimited-Control Operators

Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk.

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&nbsp;[&hellip;]

---