Theory and Pragmatics of Optimal Reduction: Logic, Linear Naming, and Programming Language Design

本研究计划研究命名和共享数据和计算线程的理论和语用学，使用最优求值和线性逻辑的原则。这些工具明确强调了在过程召回协议中必不可少的复制和丢弃操作。我们将分析最优评估的算法，盒管理的复杂性，以及具有显式控制的语言的评估语用。研究议程中还包括内涵的全抽象定理，其中术语的含义包括有关如何共享计算的操作信息，以及使用上下文语义作为流分析工具，其中所谓的“交互几何”可以提供有关过程如何访问其参数的信息。最后，我们想从线性逻辑的角度对图约简的公共系统给出一个精细化的解释，以期对最优求值中的增量计算给出一个新的范畴解释。

This research program investigates the theory and pragmatics of naming andsharing data and computation threads, using principles of optimalevaluation and linear logic. These tools explicitly highlight theoperations of copying and discarding that are essential in procedurecalling protocols. We will analyze the algorithmics of optimal evaluation, the complexity ofbox management, and the evaluation pragmatics for languages with explicitcontrol. Also included in the research agenda are intensional fullabstraction theorems, where the meaning of a term includes operationalinformation about how computations are shared, and the use of contextsemantics as a flow analysis tool, where the so-called "geometry ofinteraction" can give information about how procedures access theirarguments. Finally, we want to give a refined explanation of the bussystem of graph reduction in terms of linear logic, in the hope of giving anew categorical rendition of the incremental computation in optimalevaluation.