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

Trustees Of Boston University, Boston

Investigators

Abstract

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. We will analyze 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. Finally, we want to give 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 in optimal evaluation.