Computer Science – Programming Languages
Scientific paper
2011-03-02
LMCS 7 (2:16) 2011
Computer Science
Programming Languages
Scientific paper
10.2168/LMCS-7(2:16)2011
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\`es, 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.
Ahmed Amal
Birkedal Lars
Dreyer Derek
No associations
LandOfFree
Logical Step-Indexed Logical Relations does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Logical Step-Indexed Logical Relations, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Logical Step-Indexed Logical Relations will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-475341