Symbolic evaluation with structural recursive symbolic constants

Symbolic evaluation is a technique used for many purposes: program analysis, program verification, program transformation. The paper focusses on a novel approach which allows one to symbolically evaluate programs with respect to predicates denoting subsets of a user-defined data domain. The data domain is assumed to be recursively defined and the predicates can be defined by structural induction on the data. An application of the technique to the textual reduction of recursive programs is sketched.