Logical Step-Indexed Logical Relations
Derek Dreyer Max Planck Institute for Software Systems (MPI-SWS)
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.
The talk will be technical, but also loose and interactive; familiarity with step-indexed logical relations is not required, but depending on how much people know, we may cover more or less material. In fact, the whole point of the work is that one should be able to reap (or at least characterize) some of the benefits of step-indexed logical relations without having to manipulate/understand them directly. We'll see if that thesis holds up.
This is joint work with Amal Ahmed and Lars Birkedal, and will appear in LICS 2009. A draft version of the paper is avaiable here: