The Design, Definition, and Implementation of Programming Languages

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

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. ***