Current constructive type theories are powerful systems for describing mathematical objects with complex dependencies between types and computational values, making them expressive enough to encompass large ares of mathematics and programming. However, as the body of formal knowledge in the type theory expands, the problem of managing mathematical domains and their proofs becomes increasingly significant. Though the objects of the theory are formal, the domains are not. In this paper, we show how to apply the methods of formal data abstraction to the organization of the mathematical domains. In the process we expand the tools of data abstraction to include reusability and namespace organization, providing an environment that can be used for defining objects within a domain, for organizing domains within a type theory, and for organizing theories within a system. This environment will require extending the expressivness of inductive definitions within the type theory to include the dependent characteristics of type theoretical domains.
I wrote this paper my first year in grad school. Don't take it too seriously, and don't distribute it. I keep it online because it contains an extensive summary of the Nuprl type theory.