Subject: Paper available by ftp

From: categories <[email-masked]>
Date: Tue, 28 Feb 1995 08:44:19 -0400 (AST)

Date: Tue, 27 Feb 1996 14:17:21 -0500
From: Robert A. G. Seely <[email-masked]>

The following paper is available via ftp or WWW browser, at the URLs
given after the abstract. 

          Categories for computation in context and unified logic: I

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

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.

-----------------------------

Available via browser on my home page
  ftp://triples.math.mcgill.ca/pub/rags/ragstriples.html

or directly via ftp 
  ftp://triples.math.mcgill.ca/pub/rags/bang/context1.[ps,dvi].gz

(The [X,Y] syntax means you should use either X or Y in the URL, not both
and not the "[", "]".)