[Prev][Next][Index][Thread]
Paper available by ftp
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
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 "[", "]".)