ABSTRACT TYPES AND DEPENDENCE IN PROGRAMMING LANGUAGES

The propositions-as-types principle of Curry and Howard exhibits the close relationship between proof theory and programming language theory. This dissertation examines the programming concepts of abstract types and dependence from a logical perspective, giving a reconstruction of the type system and semantics of the programming language Russell in the Curry-Howard framework.;It begins by presenting a catalog of type theories for the lambda calculus organized by the propositions-as-types principle. These range from the positive implication calculus to a generalization of Martin-Lof's 1971 theory with type in type that includes the general sum and product type constructors. In the development of the catalog one of the most important properties considered is logical consistency; it is shown that the techniques for expressing dependence in programming languages tend to injure this property. In particular, it is shown that adding the strong interpretation of the second-order existential quantifier produces an inconsistent type theory.;After establishing the catalog as a reference point, the dissertation attacks the motivating problem--the explanation of Russell. This explanation is first done informally, then a family of dialects of Russell is extracted from the intuition. These dialects are distinguished by the rules they use to decide when two types are equal. The family ranges from a complete semantic theory of computational equality to the primitive, syntactic, criteria of being identical except for the names of bound variables. Neither of these extremes are desirable, however, since the complete equality theory fails to enforce the abstract use of abstract data types while the primitive dialect (which closely resembles the language implemented in 1980) fails to be able to express the extension of the second-order lambda calculus with dependent types. It is conjectured that there is a member of the Russell family between these two extremes that preserves abstraction. It is further conjectured that there is a consistent theory with these properties.;The dissertation concludes with a discussion of more general applications of the embedding techniques exploited here and a critique of the Russell language design.