The semantics of programs and reasoning about them are strongly influenced by the adoption of rich type disciplines. This research concerns the relationships between type systems on the one hand, and operational semantics, specification logics, correctness proof systems, and denotational semantics on the other hand. Particular attention is given to programming with limited forms of recursion enhanced by rich type disciplines, and to automated reasoning (especially rewriting techniques) about such programs relative to data type specifications. Attention is also given to the problem of matching complex data models, in particular object-oriented database models, with appropriate type systems for data manipulation languages. The integration under a statically enforceable type discipline, and in a uniform and perspicuous semantic framework, of class abstraction, inheritance, polymorphism, set manipulation, and persistence helps to increase the reliability and maintainability of database software.
