Специализатор CILPE: доказательство корректности

Специализатор CILPE преобразует программы, написанные на языке SOOL (Stack Object-Oriented Language), методом частичных вычислений. В работе доказана корректность CILPE: для любой корректной разметки исходной программы генератор остаточных программ строит остаточную программу, эквивалентную исходной при заданных значениях S-аргументов и любых значениях D-аргументов.