Effectful applicative similarity for call-by-name lambda calculi

We introduce a notion of applicative similarity in which not terms but monadic values arising from the evaluation of effectful terms, can be compared. We prove this notion to be fully abstract whenever terms are evaluated in call-by-name order. This is the first fullabstraction result for such a generic, coinductive methodology for program equivalence.