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.