Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)

Ugo Dal Lago, Francesco Gavazzo, Paul Blain Levy

We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $\lambda$-calculi with algebraic effects. We first of all endow a computational $\lambda$-calculus with…