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.