Logical relations are a promising proof technique for establishing many important properties of programs, programming languages, and language implementations. They have been used to show type safety, to prove that one implementation of an abstract data type (ADT) can be safely replaced by another, to show that languages for information-flow security ensure confidentiality, and to establish the correctness of compiler transformations and optimizations.

Yet, despite three decades of research and much agreement about their potential benefits, logical relations have only been applied to “toy” languages, because the method has not easily scaled to important linguistic features, including recursive types, mutable references, and (impredicative) generics. Previous approaches have tried to address some of these features through sophisticated mathematical machinery (domain or category theory) which makes the results difficult to formalize and/or extend.

In this talk, I will describe step-indexed logical relations which support all of the language features mentioned above and yet permit simple proofs based on operational reasoning, without the need for complicated mathematics. To illustrate the effectiveness of step-indexed logical relations, I will discuss three new contexts where I have been able to successfully apply them: secure multi-language interoperability; imperative self-adjusting computation, a mechanism for efficiently updating the results of a computation in response to changes to some of its inputs; and security-preserving compilation, which ensures that compiled code is no more vulnerable to attacks launched at the level of the target language than the original code is to attacks launched at the level of the source language.