The specializer CILPE, based on partial evaluation, transforms programs written in SOOL, a Stack Object-Oriented Language. In the paper the correctness of CILPE is proven: if the annotations in a source program are correct, the residual program generator produces a residual program that is equivalent to the source one for the specified values of the S-arguments and any values of D-arguments.
