The Design, Definition, and Implementation of Programming Languages

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

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

9804014 Reynolds The main goal is the design of a purely functional programming language with a sufficiently refined type structure to give the programmer explicit control over storage allocation. The proposed starting point is Benton's logic LNL, which integrates the computational lambda calculus of Moggi with a language using linear types. It should be possible to implement a language based on LNL so that linear values do not need garbage collection or reference counts, and so that the user has explicit control over the choices between linear and nonlinear values, and between call by value and call by name. Further possibilities include the ability to "freeze" a linear structure temporarily (which would prohibit updating while permitting multiple references), the inclusion of types for specifying in-place algorithms, and an extension to permit concurrent processes whose interaction can yield nondeterminate results. Additional topics that may be pursued are: the unification and generalization of approaches to reasoning about side effects, aliasing, and interference, the modeling of polymorphic types by means of partial equivalence relations on Scott domains, and the investigation of the relationship between partial equivalence relations on domains and information systems. ***

9804014 Reynolds 主要目标是设计一种纯函数式编程语言，具有足够精致的类型结构，使程序员能够显式控制存储分配。所提出的起点是 Benton 的逻辑 LNL，它将 Moggi 的计算 lambda 演算与使用线性类型的语言集成在一起。应该可以实现基于 LNL 的语言，以便线性值不需要垃圾收集或引用计数，并且用户可以显式控制线性值和非线性值之间以及按值调用和按名称调用之间的选择。进一步的可能性包括暂时“冻结”线性结构的能力（这将在允许多个引用的同时禁止更新）、包含用于指定就地算法的类型，以及允许其交互可以产生不确定结果的并发进程的扩展。可能追求的其他主题包括：副作用、混叠和干扰推理方法的统一和概括，通过斯科特域上的部分等价关系对多态类型进行建模，以及部分等价关系之间关系的研究关于领域和信息系统。 ***