Сергей Романенко » Публикация

Поделиться публикацией:
Опубликовать в блог:
Опубликовано 2010-01-27 Опубликовано на SciPeople2010-03-13 11:08:25 ЖурналLecture Notes in Computer Science

Proving the Equivalence of Higher-Order Terms by Means of Supercompilation
Ilya Klyuchnikov, Sergei Romanenko / Сергей Романенко
Ilya Klyuchnikov and Sergei Romanenko. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation. In: Perspectives of Systems Informatics (Proceedings of Seventh International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009). Novosibirsk: A.P. Ershov Institute of Informatics Systems, 2009, pages 150-158.
Аннотация One of the applications of supercompilation is proving properties of programs. We focus in this paper on a specific task: proving term equivalence for a higher-order lazy functional language. The "classical" way to prove equivalence of two terms t1 and t2 is to write an equality function equals and to simplify the term (equals t1 t2). However, this works only when certain conditions are met. The paper presents another approach to proving term equivalence by means of supercompilation. In this approach we supercompile both terms and compare supercompiled terms syntactically. Some applications of the technique are discussed. In particular, one of these applications may lead to the development of a more powerful "higher-level" supercompiler.
Ключевые слова публикации:


Вам необходимо зайти или зарегистрироваться для комментирования
Этот комментарий был удален
Этот комментарий был удален