[Prev][Next][Index][Thread]

Revision of paper on ftp


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]


We wish to announce the following (revised) paper now available on
triples:
 

      CATEGORIES FOR COMPUTATION IN CONTEXT AND UNIFIED LOGIC
 
         by R.F. Blute, J.R.B. Cockett, and R.A.G. Seely
 
 
ABSTRACT
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.
 
Context is represented by the classical zone on the left of the turnstile
in unified logic.  To model the classical zone to the right of the
turnstile, it is necessary to introduce a notion of cocontext.  This
results in a fibrational fork over context and cocontext and leads to
the notion of a bicontext category.  When we add the structure of a
weakly distributive category in a suitably fork fibred manner, we obtain
a model for a core fragment of unified logic.
 
We describe the sequent calculus for the fragment of unified logic
modelled by context categories; cut elimination holds for this fragment.
Categorical cut elimination also is valid, but a proof of this fact is
deferred to a sequel.
 
REMARKS
This is a completely revised version of the paper we announced in
February this year.  At the suggestion of an anonymous referee, we have
dropped all reference to the circuits of the system we originally
described, and extended the system to include multiple-conclusions as
well as multiple-hypotheses in the sequent calculus, in both the
"classical" and "linear" positions.  This is the heart of the system LU
of Girard, and a recipe is given to allow further extensions.  We plan
to describe the circuits (proof nets) for the expanded system in a
sequel, which will allow shorter and clearer proofs of categorical cut
elimination, as well as comparisons with other systems (such as our own
weakly distributive categories with storage and Bierman's MELL).
 
Since the original paper contains some material not carried over to the
revision - most significantly, the sequent calculus for the single-
conclusion logic (the "intuitionist" case), plus the proof circuits for
that logic - it remains on the ftp site with a different name and link.
 
FTP and WWW locations:
The paper may be found at this URL:
   ftp://triples.math.mcgill.ca/pub/rags/bang/context1.[dvi,ps].gz
(The earlier version is ...context0... at the same place.)
You can also get it from my WWW page:
   http://www.math.mcgill.ca/~rags
 
As you can see from the URL above, the dvi and ps files are gzipped -
if you save the files (in binary) format, gunzip them with the command
gunzip <file.name>  -- email me if you need help.

Rick Blute
Robin Cockett
Robert Seely 
( contact person for ftp help:
  rags@math.mcgill.ca )