[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear all, It is well-known that applicative bisimilarity is fully abstract on the untyped call-by-value λ-calculus. A direct consequence of that is that contextual equivalence can be restricted to applicative contexts (namely contexts defined by the grammar E ::= [-] | Ev) leaving its discriminated power unchanged. Such a result is, in principle, independent of applicative bisimilarity and I was wondering if any of you is aware of any direct (i.e. not going through applicative bisimilarity) proof that applicative contexts suffice to characterise contextual equivalence. Thanks a lot in advance! Best, Francesco Gavazzo and Ugo Dal Lago
