Reasoning about local variables with operationally-based logical relations

A parametric logical relation between the phrases of an Algol-like language is presented. Its definition involves the structural operational semantics of the language, but was inspired by recent denotationally-based work of O´Hearn and Reynolds on translating Algol into a predicatively polymorphic linear lambda calculus. The logical relation yields an applicative characterisation of contextual equivalence for the language and provides a useful (and complete) method for proving equivalences. Its utility is illustrated by giving simple and direct proofs of some contextual equivalences, including an interesting equivalence due to O´Hearn which hinges upon the undefinability of `snapback´ operations (and which goes beyond the standard suite of `Meyer-Sieber´ examples). Whilst some of the mathematical intricacies of denotational semantics are avoided, the hard work in this operational approach lies in establishing the `fundamental property´ for the logical relation-the proof of which makes use of a compactness property of fixpoint recursion with respect to evaluation of phrases. But once this property has been established, the logical relation provides a verification method with an attractively low mathematical overhead