Normal-form bisimulation, also known as open bisimulation, is a coinductive technique for higher-order program equivalence in which programs are compared by looking at their essentially infinitary tree-like normal forms, i.e. at their Böhm or Levy-Longo trees. The technique has been shown to be useful not only when proving metatheorems about lambda-calculi and their semantics, but also when looking at concrete examples of terms. In this paper, we show that there is a way to generalise normal-form bisimulation to calculi with algebraic effects, à la Plotkin and Power. We show that some mild conditions on monads and relators, introduced by Dal Lago, Gavazzo, and Levy, are enough to prove that the obtained notions of bisimulation are congruences, thus sound for contextual equivalence. We exemplify the technique for various kinds of effects, including probabilistic choice, global store, and the ticking monad.
Tue 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination ESOP Link to publication | ||
14:30 30mTalk | Effectful Normal-Form Bisimulation ESOP Link to publication | ||
15:00 30mTalk | On the Multi-Language Construction ESOP Link to publication | ||
15:30 30mTalk | Probabilistic Programming Inference via Intensional Semantics ESOP Link to publication |