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

点击翻译按钮获取中文摘要

This research program investigates the theory and pragmatics of naming and sharing data and computation threads, using principles of optimal evaluation and linear logic. These tools explicitly highlight the operations of copying and discarding that are essential in procedure calling protocols.The project analyzes the algorithmics of optimal evaluation, the complexity of box management, and the evaluation pragmatics for languages with explicit control. Also included in the research agenda are intensional full abstraction theorems, where the meaning of a term includes operational information about how computations are shared, and the use of context semantics as a flow analysis tool, where the so-called "geometry of interaction" can give information about how procedures access their arguments. A further investigation of ``superposition'' phenomena that occur in high-level sharing is planned. The final component seeks a refined explanation of the bus system of graph reduction in terms of linear logic, in the hope of giving a new categorical rendition of the incremental computation that characterizes optimal evaluation.