Computer science has become increasingly concerned with the concept of type. From the 60's onward this notion has demonstrated its value as an effective organizing concept_first in programming and programming languages, then in knowledge representation, in automated reasoning, in formal methods, and now perhaps in computer algebra systems. Previous NSF-supported research has led to a coherent family of constructive type theories and to the implementation of them in the Nuprl system from Cornell and related systems elsewhere. The plan of the investigation is to find the right concepts to explain the use of types in computer algebra systems and in formalizations of abstract computational mathematics (especially algebra). It is conjectured that in some cases the right concepts are generalizations of algebraic data types to higher-order ADT's. In other cases, new type constructors may be necessary, such as the very dependent types. These concepts are expected to clarify both pragmatic issues and foundational questions. Moreover, the method of investigation seeks to formalize the object oriented features of algebra systems and generalize them to other programming environments. The result of this research enables the design of a new generation of computer system that integrates subsystems (such as compilers, concrete and symbolic evaluators, transformation systems, provers, and data base managers) around a rich notion of type used to specify and verify the linking protocols. Investigation of computational type theory also deepens understanding of the foundations of computer science and its links to mathematics and computational science.
