Copenhagen Programming Language Seminar


Eager Normal Form Bisimulation for Sequential Control and State

Kristian StÝvring, PhD student ,
Aarhus University

Thursday, November 30th, Time: 15:00 - 16:00 (!)
IT University of Copenhagen, Rued Langgaards Vej 7, Auditorium 4


We present a new normal form bisimulation theory for the untyped call-by-value lambda calculus extended with continuations and mutable references. The associated bisimulation proof principle is sound and complete with respect to contextual equivalence. We demonstrate that this proof principle is furthermore easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.

Normal form bisimulation is based on symbolic evaluation of open terms to normal forms. It does not involve any universal quantification over function arguments and is therefore, in some respects, a more powerful proof principle for proving equivalences between recursive higher-order functions than other operationally-based syntactic methods.

This work is joint with Soren Lassen; it is to be presented at POPL'07.

Scientific host: Lars Birkedal. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org