Presidential Young Investigator Award (Computer Research): Programming Language Features Within a Type-Theoretic Frame-work

形式化方法，传统上用于逻辑或自然语言的数学分析，已被证明在计算机科学的几个分支中很有用。这里的兴趣是使用形式化系统来研究当代编程语言，其总体目标是更精确地理解当前的概念，并利用这种理解为未来设计更简单、更具表现力的语言。作为一种探索实用问题的方法，它计划组装一个“编程语言工作台”，包括一个交互式的、可编程的前端，比如Cornell Synthesizer Generator，和一个标准的增量代码生成器。在另一个方向上，与数据库和知识表示系统有关的逻辑和语言问题将受到关注。编程语言研究中的一个问题是缺乏标准术语，这反映了计算隐喻的巨大多样性。例如，Smalltalk使用“对象”和“消息”的比喻来表示，而Prolog通常被解释为来自规范的程序合成。方法之间的差异使得比较或组合不同语言的特征，或评估这种组合的危害和好处变得困难。描述可计算值的各种类型符号，通常称为“类型理论”或“类型lambda演算”，近年来引起了越来越多的关注。这些系统通常定义简单，没有与实现考虑相关的特别语法限制，并且具有足够的表达能力，可以作为理论分析和实际实现的中间语言。早期关于指称语义的工作帮助建立了简单类型lambda演算和类algol语言之间的联系，而最近的工作将这种观点扩展到具有多态函数和数据类型声明的语言中，并将这种方法改进为更实用的方法。计划继续研究类型化lambda演算的数学性质，并努力将这些系统应用于编程语言的分析和设计。特别是，计划开设一门关于程序设计语言理论及其应用的现代课程，并使用类型化λ演算的框架来分析当代语言特征，如类层次结构和方法继承。

Formal methods, as traditionally used in the mathematical analysis of logic or natural language, have proven useful in several branches of computer science. Here the interest is in using formal systems to study contemporary programming languages, with general aims towards understanding current concepts more precisely, and using this understanding to design simpler and more expressive languages for the future. As a means for exploring pragmatic issues, it is planned to assemble a "programming language work bench" comprising an interactive, programmable front-end, such as the Cornell Synthesizer Generator, and a standard incremental code generator. In another direction, logical and linguistic problems related to database and knowledge representation systems will receive attention. One problem in the study of programming languages is the lack of standard terminology, which reflects a great diversity among computational metaphors. For example, Smalltalk is presented using a metaphor of "objects" and "messages", while Prolog is often explained as program synthesis from specifications. The differences between approaches makes it difficult to compare or combine features of different languages, or to evaluate the hazards and benefits of such combinations. Various typed notations for describing computable values, often called "type theories" or "typed lambda calculi" have attracted increasing attention in recent years. These systems are generally simply defined, without ad hoc syntactic restrictions related to implementation considerations, and sufficiently expressive to serve as intermediate languages for both theoretical analysis and practical implementation. Early work on denotational semantics helped establish a connection between simple typed lambda calculus and the Algol-like languages, while more recent work has both extended this view to languages with polymorphic functions and data type declarations, and refined the approach to be more practically useful. It is planned to continue research into the mathematical properties of typed lambda calculi, and efforts to apply these systems to programming language analysis and design. In particular, it is planned to develop a modern course on programming language theory and its application, and use the framework of typed lamdga calculus to analyze contemporary language features such as class hierarchies and method inheritance.