The Design, Definition, and Implementation of Programming Languages

该项目对编程语言的设计、定义和实现进行研究，重点放在类型结构和弥合函数式编程和命令式编程之间的差距。在研究如何实现Forsythe编程语言的过程中，探讨了对交叉类型进行类型检查的较好方法。使用自顶向下的算法而不是目前的自底向上算法，预期会有相当大的改进。还研究了实现过程的一种更灵活的方法，其中过程体的一部分被编译为封闭代码，而过程体的其余部分在每个调用站点被编译为内联代码。这有望大大减轻与按名称调用相关的开销。这项研究试图统一使编程语言研究复杂化和分裂的两个棘手的二分法。目标是统一基于域的语义，它允许部分和无限的计算，与基于部分等价关系和直觉型理论的语义，它仅限于总是终止的计算。还研究了早期在类algol语言中干扰的语法控制方面的工作与最近基于线性逻辑的低级函数语言的发展的统一。特别是，本研究将被动类型的概念与线性逻辑的模态算子联系起来。

This project conducts research on the design, definition, and implementation of programming languages, with emphasis on type structure and on bridging the gap between functional and imperative programming. In studying how to implement the programming language Forsythe, it investigates better methods of type checking for intersection types. Considerable improvement is expected from using a top-down rather than the present bottom- up algorithm. A more flexible approach to the implementation of procedures is also investigated, where a portion of the procedure body is compiled into closed code while the rest of the body is compiled into inline code at each call site. This is expected to substantially alleviate the overhead associated with call by name. The research seeks to unify two of the intractable dichotomies that complicate and divide the study of programming languages. The goal is to unify semantics based on domains, which permits partial and infinite computations, with semantics based on partial equivalence relations and intuitionistic type theory, which is limited to always-terminating computations. Also investigated is the unification of earlier work on the syntactic control of interference in Algol-like languages with the more recent development of low-level functional languages based on linear logic. In particular, this research would connect the concept of passive types with the modal operators of linear logic.