Next: The Connectivity Problem Up: Introduction Previous: The Basic Problems
Research Program
Our plan is to build on our experience with mathematical software to create an integrated software environment for scientific/mathematical problemsolving. The important ideas behind our approach can be summarized as follows:

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.

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.

Adopt formal semantics for our MathBus, thus allowing
explanations of mathematical software. An explanation is a
specification of pre and postconditions 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.

Exploit the possibility of building a database of mathematical
objects. Once tools can interoperate 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 toolkit 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 HewlettPackard's FORTRAN compiler for the HPPA 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 meshgeneration 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.
Next: The Connectivity Problem Up: Introduction Previous: The Basic Problems
nuprl project
Tue Nov 21 08:50:14 EST 1995