This work is concerned with the development of a prescriptive type system for logic programs, i.e., one in which types are explicitly declared by the programmer. The system is quite expressive in that it supports parametric polymorphism, subtypes, and a new notion called bipartisan predicate types that facilitates the use of subtypes. These features make it possible to impose types on a wide range of realistic Prolog programs. The research includes the development of the theoretical foundations of the system, the design and implementation of type checking and inferencing algorithms, and the application of the system to compile-time optimization, in particular, to current NSF-supported work on the automatic parallelization of logic programs. The work is intended to impact both software development technology and compiler technology.
