Lars
Birkedal
IT University of
Copenhagen
Relational Reasoning for Recursive Types
and References
Abstract:
We present a local relational reasoning method for reasoning about
contextual equivalence of expressions in a lambda calculus with
recursive types and general references. Our development builds on the
work of Benton and Leperchey, who devised a nominal semantics and a
local relational reasoning method for a language with simple types and
simple references. Their method uses a parameterized logical relation.
Here we extend their approach to recursive types and general
references. For the extension, we build upon Pitts’ and Shinwell’s work
on relational reasoning about recursive types (but no references) in
nominal semantics. The extension is non-trivial because of
general references (higher-order store) and makes use of some new ideas
for proving the existence of the parameterized logical relation and for
the choice of parameters.
This is joint work with Nina Bohr.
Host: Karl Crary
Appointments: Margaret Weigand <weigand@cs.cmu.edu>
Wednesday, October 25, 2006
3:30 p.m.
Wean
Hall 8220
Principles
of Programming Seminars