[TYPES] Full abstraction of applicative contexts in call-by-value

[Paul Levy]

Dear Francesco,
This is the “U” part of the so-called CIU theorem, due to Mason and Talcott.  It seems to be a fundamental result, as versions of it hold in many different settings, including languages with local state and nondeterminism.  Soren Lassen’s thesis gives a good account in a nondeterministic setting:
https://urldefense.com/v3/__https://www.brics.dk/DS/98/2/BRICS-DS-98-2.pdf__;!!IBzWLUs!UrVwMt1-NZjJ9iyNJANkWYWHpY9-g9Ei6po0wyxnKTlmN920huODGRYEz1_ZGVbJO2y2IRgkg5LJhXMLg8hqyrrQDmUptTqL$ 
Best wishes,
Paul


From: Types-list <types-list-bounces at LISTS.SEAS.UPENN.EDU> on behalf of Francesco Gavazzo <francesco.gavazzo at gmail.com>
Date: Friday, 19 May 2023 at 10:57
To: Types list <types-list at lists.seas.upenn.edu>
Subject: [TYPES] Full abstraction of applicative contexts in call-by-value
CAUTION: This email originated from outside the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.


[ 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