A Concrete Representation of Observational Equivalence for PCF
classification
💻 cs.LO
keywords
innocentrepresentationequatesindistinguishableinnocentlyobservationalquantificationstrategies
read the original abstract
The full abstraction result for PCF using game semantics requires one to identify all innocent strategies that are innocently indistinguishable. This involves a quantification over all innocent tests, cf. quantification over all innocent contexts. Here we present a representation of innocent strategies that equates innocently indistinguishable ones, yielding a representation of PCF terms that equates precisely those terms that are observational equivalent.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.