Thu Jul 6, 2006, 11:00-12:00pm, 4549 Boelter Hall

Reasoning About Higher-Order Procedures and Local Storage

Mitcell Wand
Northeastern University

Current methods for reasoning about programs with higher-order procedures
and local storage are limited in their abilities.  Reasoning about
these features is vital for dealing with programs in object-oriented
languages, since these features are
necessary for modelling instance variables and callbacks.

In recent work, we have developed methods, based on bisimulation, for
proving equivalences between program fragments in languages with
higher-order procedures and local storage.  We have obtained results
that have been difficult or impossible to prove using existing
methods.

We will present a tutorial on how these methods work in the simple case of
the untyped call-by-value lambda calculus, and sketch the extension to
imperative languages.

[Joint work with Vasilieos Koutavas.  Some of this work was reported
at POPL 2006 and ESOP 2006.]

Host: Jens Palsberg