Categories for computation in context and unified logic Original Research Article

In this paper we introduce context categories to provide a framework for computations in context. The structure 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. These zones may be modelled categorically as a context/computation separation given by a fibration. The perspective leads to an analysis of the exponential structure of linear logic using strength (or context) as the primitive notion.