DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

Eager Normal Form Bisimulation

Soren B. Lassen,
Google Inc.

Monday (!), September 5, 11:15-12:00
DIKU, Universitetsparken 1, in the small auditorium

Abstract:

This talk describes a new bisimulation equivalence for the pure untyped call-by-value lambda-calculus, called enf bisimilarity. It is based on eager reduction of open terms to eager normal form (enf) and can be viewed as the call-by-value analogue of Boehm tree equivalence. Enf bisimilarity is the congruence on source terms induced by the call-by-value CPS transform and Boehm tree equivalence on target terms. Enf bisimilarity enjoys a powerful bisimulation proof principle which, among other things, can be used to establish a retraction theorem for the call-by-value CPS transform.

Appeared in: LICS 2005: 20th Annual IEEE Symposium On Logic In Computer Science, Chicago, IL, June, 2005. http://soren.blassen.dk/papers/2005lics.pdf

Scientific host: Olivier Danvy. 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