RUI: Semantics and Design of Object-Oriented Languages

该奖项是对静态类型面向对象编程语言的设计和语义的研究。该项目有几个目标。(1)它构建并扩展了多态、静态类型的面向对象编程语言PolyTOIL的设计，以提供更强大的功能和可表现性，同时保持类型安全。(2)研究了一种面向对象语言的设计，其类型之间的主要关系是匹配而不是子类型。这可能需要开发部分类型推断系统，以允许程序员避免绑定类型参数的扩散。(3)寻求为面向对象语言的基础演算创建更好的数学(外延)模型。(4)研究了面向对象程序设计语言验证技术的发展。(5)将当前面向对象语言的语义知识应用到并发面向对象语言的理解中。这些问题正在使用类型检查规则和操作语义的形式规范进行攻击。主题约简风格的定理被用来证明类型系统的安全性。编写口译程序是为了更好地了解该系统的长处和短处，并鼓励将理论设计扩大到全功能编程语言。该项目试图通过证明操作语义和公理语义的一致性来验证验证技术。

This award is for research on the design and semantics of statically-typed object-oriented programming languages. The project has several goals. (1) It builds on and extends the design of the polymorphic, statically-typed object-oriented programming language, PolyTOIL, to provide more power and expressibility while retaining type-safety. (2) It investigates the design of an object-oriented language whose primary relation between types is matching rather than subtyping. This will likely req uire the development of a partial type-inference system to allow the programmer to avoid the proliferation of bounded type parameters. (3) It seeks to create better mathematical (denotational) models for foundational calculi for object-oriented languages. (4) It investigates the development of verification techniques for object-oriented programming languages. (5) It applies current knowledge of the semantics of object-oriented languages to the understanding of concurrent object-oriented languages. These problems are being attacked using formal specifications of type-checking rules and operational semantics. Subject-reduction-style theorems are being used to prove the safety of type systems. Interpreters are being written in order to provide a better understanding of the strengths and weaknesses of the systems and in order to invetigate scaling up of theoretical designs to full-strength programming languages. The project seeks to validate verification techniques by proving the consistency of an operational and axiomatic semantics.