Derek Dreyer ; Amal Ahmed ; Lars Birkedal - 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 RelationsArticle

Authors: Derek Dreyer ; Amal Ahmed ORCID; Lars Birkedal

    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
    Imported on: January 8, 2010
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,D.3.3, F.3.1, F.3.3

    34 Documents citing this article

    Consultation statistics

    This page has been seen 2153 times.
    This article's PDF has been downloaded 485 times.