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

形式化方法，传统上用于数学分析， 逻辑或自然语言，已被证明是有用的几个分支， 计算机科学 这里的兴趣在于使用正式系统来 学习当代编程语言，总体目标是 更准确地理解当前的概念，并利用这一点， 设计更简单，更有表现力的语言， 未来 作为探讨务实问题的一种手段， 组装“编程语言工作台”， 可编程前端，如康奈尔合成器发生器，以及 一个标准的增量代码生成器。 在另一个方向，逻辑 与数据库和知识有关的语言问题 代表制度将受到重视。 编程语言研究中的一个问题是缺乏 标准术语，反映了 计算隐喻 例如，Smalltalk是使用 隐喻的“对象”和“消息”，而Prolog往往是解释 从规范中进行程序合成。 之间的差异 方法使得难以比较或联合收割机的特征， 不同的语言，或评估的危害和利益， 组合。 用于描述可计算值的各种类型化表示法，通常称为 “类型理论”或“类型化lambda演算”吸引了越来越多的 近年来的关注。 这些系统通常被简单地定义， 没有与实现相关的特别语法限制 考虑因素，并充分表达作为中间 语言的理论分析和实际执行。 指称语义学的早期工作帮助建立了 简单类型lambda演算和类Algol语言之间的区别， 虽然最近的工作都将这一观点扩展到语言， 多态函数和数据类型声明，并改进了 方法更实用。 计划继续 研究类型化lambda演算的数学特性，以及 努力将这些系统应用于编程语言分析， 设计 特别是，计划开发一个现代课程， 程序设计语言理论及其应用，并使用框架 类型lamdga演算来分析当代语言特征， 类层次结构和方法继承。

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.