#
Categories for computation in context and unified logic:
the "intuitionist" case

by R.F. Blute, J.R.B. Cockett, and R.A.G. Seely

This is an early version of the paper, dealing with the "intuitionist" case.
That is, the case where only single-formula conclusions are permitted.
The full version is now available.
The full version has no discussion of the "intuitionist" case, but proceeds
directly to the full case. In addition, the full version has none of the
discussion of proof circuits that occupies the final sections of the
original version of the paper. Proof circuits for the full calculus will be
covered in a sequel.

#### Abstract

In this paper we introduce the notion of contextual categories.
These provide a categorical semantics for the modelling of
computation in context, based on the idea of separating logical sequents
into two zones, one representing the context over which the computation
is occurring, the other the computation itself. The separation into
zones is achieved via a bifunctor equipped with a tensorial
strength. We show that a category with such a functor can be viewed as
having an action on itself. With this interpretation, we obtain a
fibration in which the base category consists of contexts, and the
reindexing functors are used to change the context.

We further observe that this structure also provides a framework for
developing categorical semantics for Girard's Unified Logic, a key
feature of which is to separate logical sequents into two zones, one in
which formulas behave classically and one in which they behave linearly.
This separation is analogous to the context/computation separation
above, and is handled by our semantics in a similar fashion.
Furthermore, our approach allows an analysis of the exponential
structure of linear logic using a tensorially strong action as the
primitive notion. We demonstrate that from such a structure one can
recover a model of the linear storage operator.

Finally, we introduce a sequent calculus for the fragment of Unified
Logic modeled by contextual categories. We show cut elimination for
this fragment, and we introduce a simple notion of proof circuit, which
provides a description of free contextual categories.