For what languages is there already a theory of observational equivalence? For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to use the notion, not to investigate it for its own sake.

This notion should be "extensional" — in particular, to prove that $t_1 \cong t_2$, it should be enough to prove that $t_1\; v \cong t_2\; v$ for all values $v$ of the appropriate type.

Denotational equivalence

Denotational equivalence easily satisfies all the right lemmas, but a denotational semantics for arbitrary PTS seems rather challenging — it'd appear hard already for System F.

Contextual/observational equivalence

The obvious alternative are then various forms of contextual equivalence (two terms are equivalent if no ground context can distinguish them), but its definition is not immediately usable; the various lemmas aren't trivial to prove. Have they been proved for PTS? Alternatively, would the theory be an "obvious extension", or is there reason to believe the theory would be significantly different?

EDIT: I didn't say what's hard above.

Easy part: the definition

Defining the equivalence is not too hard, and the definition appears in many papers (starting at least from Plotkin 1975's study of PCF, if not earlier — the source might be Morris's PhD thesis from 1968).
We $t_1 \cong t_2$ if for all ground contexts $C$, $C[t_1] \simeq C[t_2]$ — that is, $C[t_1]$ and $C[t_2]$ give the same result. You have a few choices here with lots of alternatives: For instance, in a strongly normalizing language, if you have a ground type of naturals, you can say that ground contexts are the ones that return naturals, and then $a \simeq b$ means that $a$ and $b$ evaluate to the same number. With nontermination, for reasonable languages it is enough to use "X terminates" as observation, because if two programs are equivalent when observing termination, they're also equivalent when observing the result.

Hard part: the proofs

However, those papers often don't explain how hard it is to actually use this definition. All the references below show how to deal with this problem that, but the needed theory is harder than one thinks. How do we prove that $t_1 \cong t_2$? Do we actually do case analysis and induction on contexts? You don't want to do that.

As Martin Berger points out, you want to use, instead, either bisimulation (as done by Pitts) or a logical equivalence relation (that Harper simply calls "logical equivalence").

Finally, how do you prove extensionality as defined above?

Harper solves these questions in 10 pages for System T, through considerable cleverness and logical relations. Pitts takes more. Some languages are yet more complex.

How to deal with this

I'm actually tempted to make my proofs conditionally on a conjectured theory of equivalence for PTS, but the actual theories require nontrivial arguments, so I'm not sure how likely such a conjecture would be to hold.

I'm aware (though not in detail) of the following works:


Andrew Pitts (for instance in ATTAPL for an extended System F, and in a few papers, such as the 58-page "Operationally-Based Theories of Program Equivalence").
Practical Foundations of Programming Languages (chapters 47-48), which is inspired by Pitts (but claims to have simpler proofs).
A logical study of program equivalence. I can't find an English abstract, but it seems to spend a great deal of effort for side effects (references), which seems an orthogonal complication.
A compositional denotational semantics $[\![ {-} ]\!]$ of a programming language (a domain-theoretic or game-theoretic one, for instance) is adequate if semantically equal terms imply that they are observationally equivalent:
$$[\![ t_1 ]\!] = [\![ t_2 ]\!] \implies t_1 \cong t_2.$$
It often happens that it is far easier to calculate denotations that to prove observational equivalence. This is a common technique with many known variants. Adequacy is defined already in Plotkin's PCF paper.