Presidential Young Investigator Award: Type Disciplines in Programming Language Design

程序的语义和有关它们的推理受到丰富类型规则的采用的强烈影响。本研究一方面关注类型系统与操作语义、规范逻辑、正确性证明系统和指称语义之间的关系。特别关注通过丰富类型规程增强的有限形式递归的编程，以及关于这类程序相对于数据类型规范的自动推理(尤其是重写技术)。还注意了将复杂数据模型，特别是面向对象的数据库模型与数据操作语言的适当类型系统相匹配的问题。类抽象、继承、多态、集合操作和持久化在可静态强制执行的类型规则下，在统一而清晰的语义框架中集成，有助于提高数据库软件的可靠性和可维护性。

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.