Some of the work we propose requires careful theoretical analysis and design. For example, a proposal we have made for linking HOL and Nuprl required a new analysis of the foundations of computational type theories. Howe [] was able to show that a substantial subset of the Nuprl type theory was consistent with HOL. We can use the module mechanisms for the library to enforce this subset in the link to HOL. There is work to be done in extending Howe's analysis to other type constructors such as intersection types and recursive types. To begin a study of links to PVS, we need to analyze that type theory and related it to subsets of the computational type theories.