Dreyer, Derek and Ahmed, Amal and Birkedal, Lars - Logical Step-Indexed Logical Relations

lmcs:698 - Logical Methods in Computer Science, June 7, 2011, Volume 7, Issue 2 - https://doi.org/10.2168/LMCS-7(2:16)2011
Logical Step-Indexed Logical Relations

Authors: Dreyer, Derek and Ahmed, Amal and Birkedal, Lars

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.

Volume: Volume 7, Issue 2
Published on: June 7, 2011
Submitted on: January 8, 2010
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,D.3.3, F.3.1, F.3.3


Consultation statistics

This page has been seen 308 times.
This article's PDF has been downloaded 128 times.