RISC Forum

In this thesis we try to improve on four aspects of the differential part of differential characteristic set theory.

The most important contribution is a clear and rigorous separation between used programs and their specifications, while presenting the theory of the differential part of differential characteristic set computations in a mostly self-contained fashion. Although the formulations used in current literature might suggest that there is already such a separation between programs and their specifications, we give several counter-examples to this impression.

Secondly, instead of using just one set of requirements for differential reduction, we present and use several different kinds of specifications and can thereby precisely describe what requirements are needed for each of the occurrences of differential reduction.

Thirdly, we promote constants to first-class citizens of differential characteristic set theory.

Finally, we give a generalization of coherence and a corresponding Rosenfeld Lemma.