Logical Step-Indexed Logical Relations
Source: IT University of Copenhagen
The authors 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, they 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. They 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, they derive a useful set of rules with which they can prove contextual (in-)equivalences without mentioning step indices.