Presidential Young Investigator Award: Type Disciplines in Programming Language Design

总统青年研究员奖：编程语言设计的类型学科

• 批准号: 9057570
• 负责人: Val Tannen
• 金额: $ 27.88万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-08-15 至 1997-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9057570&HistoricalAwards=false
• 关键词: Presidential; Young; Investigator; Award; Type

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.

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