Logical Step-Indexed Logical Relations

We show how to reason about "step-indexed" logical relations in an abstract way, avoiding the tedious, error-prone, and proof-obscuring step-index arithmetic that seems superficially to be an essential element of the method. 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 et al.\´s "very modal model" paper. We encode in LSLR a logical relation for reasoning (in-)equationally about programs in call-by-value system F extended with recursive types. Using this logical relation, we derive a useful set of rules with which we can prove contextual (in-)equivalences without mentioning step indices.