Logical Step-Indexed Logical Relations

Abstract

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.

Cited by in corpus (11)

• Step-Indexed Logical Relations for Probability (long version)
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
• Step-Indexed Relational Reasoning for Countable Nondeterminism
• A Relational Logic for Higher-Order Programs
• Bialgebraic Reasoning on Higher-Order Program Equivalence
• Almost-Sure Termination by Guarded Refinement
• Abstract Congruence Criteria for Weak Bisimilarity
• Polymorphic Typestate for Session Types
• A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential
• Logical relations for coherence of effect subtyping
• Gradual Guarantee via Step-Indexed Logical Relations in Agda