Copenhagen Programming Language Seminar
The interest of extended systems of reductions is that some computational rules are presented as reductions and this may help to obtain more efficient algorithms for equality of lambda-terms (and functions they represent). It is well known that the reasoning based on extensional equality (for example, in proof assistants) could be extremely heavy. At the same time, the attempt to add reductions based on all extensional equalities usually results in systems that are not strongly normalizing and do not have Church-Rosser property (i.e., are not convergent). We studied the possibility to add reductions related to some extensional equalities of special interest in such a way that convergence is preserved.
Andrzej Filinski. 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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org