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:Kathy McNiff <kmm@cs.cmu.edu>
Friday, May 22,
2009
3:30 p.m.
Wean
Hall 8220
Principles
of Programming Seminars