Derek Dreyer
MPI-SWS

Logical Step-Indexed Logical Relations

Abstract:
Appel and McAllester devised the "step-indexed model" in order to express "semantic" proofs of type safety for use in foundational proof-carrying code. The basic idea is to characterize type inhabitation as a predicate indexed by the number of steps of computation left before "the clock" runs out.  In subsequent work, Ahmed and coworkers have shown how to generalize the step-indexed model to binary "step-indexed logical relations", with which one may reason inequationally about programs in languages with semantically complex type structure (e.g. universal, existential, recursive and mutable reference types).  However, a continual annoyance in working with step-indexed logical relations, as well as a stumbling block to their general acceptance, is the tedious, error-prone, and proof-obscuring step-index arithmetic that seems superficially to be an essential element of the method.

In this work, we show how to reason about binary step-indexed logical relations in a more abstract, high-level way.  Specifically, we define a logic LSLR, which is inspired by Plotkin and Abadi's logic for relational parametricity, but also supports recursively defined relations by means of the modal "later" operator from Appel et al.'s "very modal model" paper.  We encode in LSLR a logical relation for reasoning (in-)equationally about programs in call-by-value System F extended with recursive types.  Using this logical relation, we derive a useful set of proof rules that allow us to harness the power of
step-indexed logical relations without counting steps.

This is joint work with Amal Ahmed and Lars Birkedal.



Host: Robert Harper
Appointments:Christine Simony <cs0i@andrew.cmu.edu>





Friday, May 22, 2009
3:30 p.m.
Wean Hall 8220

Principles of Programming Seminars