We aim to specify program transformations in a declarative style, and then to generate efficient program transformers from such specifications. Many transformations require non-trivial program analysis to check their applicability, and it is prohibitively expensive to re-run such analyses after each transformation. It is desirable, therefore, that the analysis information is incrementally updated.

We achieve this by drawing on two pieces of previous work: first, Bernhard Steffen's proposal to use model checking for certain analysis problems, and second, John Conway's theory of language factors. The first allows the neat specification of transformations, while the second opens the way for an incremental implementation. This seems to be the first application of Conway's factor theory since he invented it in the late sixties.

If time allows, we shall briefly report on an implementation in Moscow ML with the Muddy BDD package, which transforms the .NET intermediate language.