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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 16:00: Program SemanticsESOP at SUN II
Chair(s): Andrzej MurawskiUniversity of Oxford
14:00 - 14:30
Talk
ESOP
Dylan McDermottUniversity of Cambridge, Alan MycroftUniversity of Cambridge
Link to publication
14:30 - 15:00
Talk
ESOP
Ugo Dal LagoUniversity of Bologna / Inria, Francesco Gavazzo
Link to publication
15:00 - 15:30
Talk
ESOP
Samuele BuroUniversità degli Studi di Verona, Isabella MastroeniUniversity of Verona, Italy
Link to publication
15:30 - 16:00
Talk
ESOP
Simon CastellanImperial College London, UK, Hugo PaquetUniversity of Cambridge
Link to publication