It is not too much of a stretch of the imagination to say that mathematics boils down to the study of the question: When are two terms equal? (along with all of the consequences of the various answers to this question). These studies are motivated by various applications that require different variations on the notion of equality.

Programming language semantics is no different, and the study of program equivalence is a central theme. The study of equivalence of programs is well established, and techniques such as applicative bisimulation and logical relations have a distinguished history. These techniques have found applications in the area of program analysis and verification.

This paper studies a particular notion of program equivalence--linear contextual equivalence--motivated by applications in the area of language-based security, which the authors have also worked on. The authors have devised a notion of equivalence of programs where two programs are equivalent if they result in observationally equivalent programs when substituted in all possible linear contexts. Such programs are in some sense indistinguishable with respect to linear contexts.

This extrinsic notion of contextual equivalence can be characterized in terms of certain intrinsic properties of programs--this is the crux of the technical development in the paper. This intrinsic characterization is provided by a transition relation imposed on programs, showing that trace equivalence with respect to this transition relation characterizes contextual equivalence.

The techniques developed in this paper to characterize contextual equivalence are interesting in themselves and are not a straightforward consequence of techniques in the literature. They are tantalizingly similar, but there are some crucial differences--in this case, the novel concept of contextual transitions. One hopes for a follow-up work that compares and contrasts the menagerie of equivalences and techniques for studying them that are now available in the literature.