Investigations of Type Theory in Programming Logics and Intelligent Systems

Type theory has become central to computer science because it deals with fundamental issues in programming languages, in programming methodology and specification languages, in automatic theorem proving and programming logic, in natural language semantics and in the foundations of intelligent systems. At Cornell we have been studying a logical theory of types which has influenced the design of programming languages and has become the basis of an implemented program development system. This theory answers many basic questions about data types. Here we discuss three general questions about this theory: how logical types relate to domains, how they relate to sets, how they organize programming logics and the intelligent systems built around them. These issues are each of independent value, but they also arise naturally as part of a program to provide a computationally meaningful foundation to computing theory