Copenhagen Programming Language Seminar
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.
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 firstname.lastname@example.org with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org