Categories for computation in context and unified logic (Q678833)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Categories for computation in context and unified logic |
scientific article |
Statements
Categories for computation in context and unified logic (English)
0 references
12 January 1998
0 references
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.
0 references
context category
0 references
linearly distributive categories
0 references
cut-elimination
0 references
framework for computations in context
0 references
linear logic
0 references
weakly distributive categories
0 references
categorical proof theory
0 references
Girard's unified logic
0 references
fibrations
0 references
tensorial strength
0 references