Programming Language Analysis and Design

本研究关注的是理解当代编程语言的语法、操作和语义特性的框架。除了在类型论和指称语义的基础上扩展了程序设计的描述性理论外，该研究还有助于开发新的程序设计语言。编程语言的目标是提高编程的方便性和效率。这既包括更简洁的语言设计，使程序对程序员来说更容易阅读、编写和维护，也包括对功能的仔细关注，使编程工具能够有意义地操作程序。该研究的理论方面旨在为编程工具和环境的开发和实现建立语义和算法基础。贯穿研究的一个共同主线是使用类型系统，它既是用于分析的数学框架，也是用于自动程序分析的语法基础。一些具体的问题是面向对象编程语言的静态类型分析，旨在建立可用于编译和程序转换的程序属性，函数式语言的类型推断算法，包括命令式和控制特性（异常和延续），以及使用线性逻辑来获得更精确的程序静态分析。一个实用的语言设计工作是一个类型和模块系统，它对用现有语言设计和开发面向对象的程序很有用。一些较长期的基础问题是线性逻辑的模型理论，对具有高阶和多态结构的命令式程序进行推理的操作和表意方法，以及在高阶或面向对象的语言框架中处理并发性。

This research is concerned with a framework for understanding syntactic, operational and semantic properties of contemporary programming languages. In addition to extending a descriptive theory of programming based on type theory and denotational semantics, the research contributes to the development of new programming languages. The programming language goals are increased ease and efficiency of programming. This involves both cleaner language design, so that programs are easier for programmers to read, write and maintain, and careful attention to features that make it possible for programming tools to manipulate programs meaningfully. The theoretical aspects of the research are aimed at establishing the semantic and algorithmic basis for the development and implementation of programming tools and environments. A common thread through the research is the use of type systems, both as a mathematical framework for analysis and a syntactic basis for automatic program analysis. Some specific problems are the static type analysis of object-oriented programming languages, aimed toward establishing properties of programs that may be used in compilation and program transformation, type inference algorithms for functional languages that include imperative and control features (exceptions and continuations), and the use of linear logic to obtain more precise static analysis of programs. A pragmatic language design effort is a type and module system that is useful for the design and development of object-oriented programs in existing languages. Some longer-term foundational problems are the model theory of linear logic, operational and denotational methods for reasoning about imperative programs with higher-order and polymorphic constructs, and treatments of concurrency in a higher-order or object-oriented language framework.