Copenhagen Programming Language Seminar

Proving term equivalence by the means of supercompilation

Ilya Klyuchnikov
Russian Academy of Sciences, Moscow

Thursday, November 13, 2008, 15:00-16:00
DIKU North, Universitetsparken 1, Aud. Lille UP1


One of the applications of supercompilation is proving properties of programs. We focus in this presentation on a certain task: proving term equivalence for a higher-order lazy functional language. The "classical" way to prove the equivalence of two terms x and y is to write an equality function and to simplify the term equal(x,y). A different approach for proving terms equivalence by the means of supercompilation is suggested. In this approach we supercompile both terms and compare them. Applications of this approach are discussed.

Scientific host:Robert Glück Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the 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