ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 14:30 - 15:00 at SUN II - Program Semantics Chair(s): Andrzej Murawski

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 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 16:00
Program SemanticsESOP at SUN II
Chair(s): Andrzej Murawski University of Oxford
14:00
30m
Talk
Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination
ESOP
Dylan McDermott University of Cambridge, Alan Mycroft University of Cambridge
Link to publication
14:30
30m
Talk
Effectful Normal-Form Bisimulation
ESOP
Ugo Dal Lago University of Bologna / Inria, Francesco Gavazzo
Link to publication
15:00
30m
Talk
On the Multi-Language Construction
ESOP
Samuele Buro Università degli Studi di Verona, Isabella Mastroeni University of Verona, Italy
Link to publication
15:30
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
ESOP
Simon Castellan Imperial College London, UK, Hugo Paquet University of Cambridge
Link to publication