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雷诺兹的主要目标是设计一种纯函数式编程语言，具有足够精致的类型结构，使程序员能够显式控制存储分配。建议的起点是Benton的逻辑LNL，它将Moggi的计算Lambda演算与使用线性类型的语言相结合。应该可以实现一种基于LNL的语言，以便线性值不需要垃圾收集或引用计数，从而用户可以显式地控制线性和非线性值之间的选择，以及按值调用和按名称调用之间的选择。进一步的可能性包括暂时“冻结”线性结构的能力(这将在允许多个引用的同时禁止更新)，包含用于指定就地算法的类型，以及允许交互可以产生不确定结果的并发进程的扩展。其他可能追求的主题是：关于副作用、混叠和干扰的推理方法的统一和泛化，通过Scott域上的部分等价关系对多态类型进行建模，以及域和信息系统上的部分等价关系之间的关系的调查。***