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
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.


Source : oai:arXiv.org:1103.0510
DOI : 10.2168/LMCS-7(2:16)2011
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


Share

Consultation statistics

This page has been seen 99 times.
This article's PDF has been downloaded 38 times.