Research Program

Our plan is to build on our experience with mathematical software to create an integrated software environment for scientific/mathematical problem-solving. The important ideas behind our approach can be summarized as follows:

1. Design the system around a MathBus. This component provides an efficient mechanism for transmitting mathematical information of all types between software modules. In addition to the usual computational data structures such as matrices of real numbers, the MathBus supports geometric objects, symbolic expressions, differential equations, theorems, and proofs. The MathBus provides a standardized language for writing formal mathematical definitions and provides software protocols for communicating these definitions to subsystems linked to the bus. We discuss this in more detail in Section 2. The MathBus resolves the connectivity problem.

2. Support a transformation based programming methodology to develop C and Fortran codes for parallel and sequential computing. The construction of the MathBus makes the transformation based approach feasible, because we will already have in place mathematical definitions for many of the common mathematical objects (sparse matrices, geometric shapes, etc.) arising in computational science. Transformations enhance our ability to attack the code creation problem.

3. Adopt formal semantics for our MathBus, thus allowing explanations of mathematical software. An explanation is a specification of pre- and post-conditions for a computation. Such explanations are crucial to support collaboration between software packages and also between their users. The use of formal semantics resolves the explanation problem.

4. Exploit the possibility of building a database of mathematical objects. Once tools can inter-operate and mathematical models can be shared, it becomes possible to create collections of mathematical theorems, explanations, and examples and counterexamples. We intend to start a database of this kind for some interesting subarea of computational mathematics.

These four points are discussed in detail in the remaining sections of the proposal.

Our diverse team is uniquely qualified to achieve these goals. Constable brings his extensive experience with formal logic tools to bear on the proposed research. His group's Nuprl system [26] has been used for verifying hardware [2,1], formalizing mathematical theories [53] and as an aid in the study of constructive mathematics [27,85].

Chew and Zippel have both worked on the Simlab project, which is an attempt to build a comprehensive environment for engineering computation. Chew's area of expertise is computational geometry, and he has developed an advanced tool for mesh generation. Zippel's work addresses symbolic computation and transformation based programming. Zippel has developed the Weyl language for symbolic algebra.

Pingali's research area is restructuring compiler technology, and specifically, transformation based parallel programming for scientific problems. His research group has developed the Lambda loop transformation tool-kit which can be used to transform loops in FORTRAN programs with the goal of increasing parallelism or of enhancing locality of reference. This technology has been transferred to Hewlett-Packard's FORTRAN compiler for the HP-PA architecture. Pingali's group has also worked on fast algorithms for control dependence problems, and this technology has been incorporated into a production compiler by Flavors Inc; it is also being used at Microsoft.

Finally, Vavasis's area is scientific computing and numerical algorithms. He has developed algorithms for numerical solution of partial differential equations and also optimization. He is currently developing a mesh-generation software package.

The combined expertise of the five investigators covers all aspects of the proposed research. Moreover, we have already begun to collaborate on projects that extend each of our own individual expertise into the overlapping area defined by this proposal. Examples of these collaborations are described below.

In addition, we plan to continue to coordinate our activities with Cornell work on programming languages and environments [37,36,47,73,127,108,95]. In particular, the work being developed in support of the NSF proposal Software Engineering with a Transformational System by Gries and Teitelbaum is likely to supply a homogeneous user interface to the MathBus.