While syntactic logical relations have been defined and applied primarily for calculi with types, it has been occasionally demonstrated that the technique can be employed in an untyped context as well, by replacing the type structure with step-indexing. In this article, we show how untyped step-indexed logical relations can be used both to prove contextual equivalence of expressions within a single calculus and to establish strong properties of program translations from one calculus to another.

To this end, we focus on the untyped call-by-value $\lambda$-calculus extended with the standard abortive control operators call/cc and abort, for which we define biorthogonal step-indexed binary logical relations. In contrast to the existing untyped logical relations, which are defined intensionally, i.e., based on constructors, our definition is extensional, i.e., based on eliminators. Such an approach scales better to richer languages, but it poses certain technical challenges that we show how to overcome. Using these relations we verify some interesting program equivalences, one of which is known to be hard to prove with the existing techniques such as bisimulations. We then define untyped inter-language logical relations in order to present an elegant proof of the full abstraction theorem for a standard CPS translation from the calculus with control operators to (a fragment of) the pure $\lambda$-calculus.