Categories for computation in context and unified logic (Q678833)

The notion of ``context category'' is introduced, to provide a framework for computations in context. This is part of the attempt to elucidate the structure of linear logic using weakly distributive categories (recently renamed by the authors to ``linearly distributive categories'' [\textit{J. R. B. Cockett} and \textit{R. A. G. Seely}, ``Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories'', Theory Appl. Categ. 3, No. 5, 85-131 (1997); see the review below]). The present work also provides a basis for developing the categorical proof theory of Girard's unified logic. A key feature of this logic is the separation of sequents into classical and linear zones. To model categorically the classical zones at the left and right sides of the turnstile, the notions of context and cocontext are considered. Categorically, this involves fibrations and the consideration of tensorial strength. Weakly (linearly) distributive categories provide a model for a core fragment of unified logic. Cut-elimination is investigated. As a connection to explore in future work, the authors mention the ``Action Calculus'' of R. Milner.