The Design, Definition, and Implementation of Programming Languages

编程语言的设计、定义和实现

• 批准号: 9409997
• 负责人: John Reynolds
• 金额: $ 31.55万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-04-01 至 1998-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9409997&HistoricalAwards=false
• 关键词: Design; Definition; Implementation; Programming; Languages

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.

该项目对编程语言的设计，定义和实施进行了研究，重点是类型结构以及弥合功能和命令编程之间的差距。 在研究如何实施编程语言方面，它研究了更好的类型检查交叉点类型的方法。 使用自上而下而不是当前的底部算法，预计将有很大的改善。 还研究了一种更加灵活的方法，其中一部分程序主体被编译成封闭的代码，而在每个呼叫站点上将其其余部分汇编为内联代码。 预计这将大大减轻与呼叫名称相关的间接费用。 该研究试图统一两个棘手的二分法，使编程语言的研究变得复杂并分裂。 目的是基于域的语义统一语义，该域允许基于部分等价关系和直觉类型理论的语义，该语义限于始终终止计算。 还研究的是，统一了对类似Algol的语言干扰的句法控制的统一，其最新的基于线性逻辑的低级功能语言的发展。 特别是，这项研究将被动类型的概念与线性逻辑的模态操作员联系起来。