Collectively the investigators have a significant amount of experience with transformation technologies. As mentioned above, the Bernoulli project (Pingali and Zippel) includes both high level program transformations (discretizations) and the transformations required by compiler optimizations. The Nuprl proof development system (Constable) has at its core a powerful transformation system. Each of the transformation systems mentioned deals with different types of expressions. Already in the Bernoulli project, we have seen how cooperation between the discretization transformations and the code restructuring transforms used by the compiler can produce significant benefits for parallel computations. While it is not likely to be practical to create a single transformation system that is appropriate for all of these activities, we plan to combine the technologies being developed to strengthen our individual efforts. Furthermore, adapting the term structures used by the different transformation systems to the MathBus will facilitate more closely coupling the systems.
In addition, our colleagues in the Computer Science Department (Gries and Teitelbaum) are developing user interface technologies that simplify the use of expression transformation systems (see their NSF proposal Software Engineering with a Transformational System). We will take advantage of the ideas, techniques and tools they develop.