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.