SPLASH 2023 (series) / PPDP 2023 (series) / PPDP 2023 /
Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operators
Algebraic effect handlers and delimited control operations are abstractions of computational effects. Originally proposed without labels, their labeled extensions can express multiple kinds of exceptions, multiple states, and so on. We show that the two abstractions have equal expressive power. To do this, we first develop a type system for each abstraction with each label extension. We then define macro translations between two abstractions with the same label extension. The equivalences establish a strong connection between the two abstractions with labels, which can be used to understand and implement one abstraction in terms of the other.
Sun 22 OctDisplayed time zone: Lisbon change
Sun 22 Oct
Displayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 5mOther | Opening of PPDP PPDP | ||
09:05 25mPaper | A Calculus of Delayed Reductions PPDP | ||
09:30 30mPaper | Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operators PPDP Kazuki Ikemori Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology | ||
10:00 30mPaper | Comprehending queries over finite maps PPDP Wilmer Ricciotti University of Edinburgh, UK |