Appel and McAllester's "step-indexed" logical relations have proven
to be a simple and effective technique for reasoning about programs in
languages with semantically interesting types, such as general
recursive types and general reference types. However, proofs using
step-indexed models typically involve tedious, error-prone, and
proof-obscuring step-index arithmetic, so it is important to develop
clean, high-level, equational proof principles that avoid mention of
step indices.
In this paper, we show how to reason about binary step-indexed logical
relations in an abstract and elegant way. Specifically, we define a
logic LSLR, which is inspired by Plotkin and Abadi's logic for
parametricity, but also supports recursively defined relations by
means of the modal "later" operator from Appel, Melliès, Richards,
and Vouillon's "very modal model" paper. We encode in LSLR a
logical relation for reasoning relationally about programs in
call-by-value System F extended with general recursive types. Using
this logical relation, we derive a set of useful rules with which we
can prove contextual equivalence and approximation results without
counting steps.