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.