We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value λ-
calculi with algebraic effects. We first of all endow a computational λ-calculus with a monadic
operational semantics. We then show how the theory of relators provides precisely what is
needed to generalise applicative bisimilarity to such a calculus, and to single out those
monads and relators for which applicative bisimilarity is a congruence, thus a sound
methodology for program equivalence. This is done by studying Howe's method in the …

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 a monadic operational semantics. We then show how the theory of relators
provides precisely what is needed to generalise applicative bisimilarity to such a calculus,
and to single out those monads and relators for which applicative bisimilarity is a
congruence, thus a sound methodology for program equivalence. This is done by studying …