On Dec 14, 2004, at 11:03 AM, Lutz Strassburger wrote:
Hi Frogs,
We finally maged to finish our paper on proof nets for multiplicative
linear logic with units. The full version can be found here:
http://www.ps.uni-sb.de/~lutz/papers/freestaraut.pdf
Well, believe it or not, it can also be found on
http://www.loria.fr/~lamarche !!
(i'm not giving the full path so you wil have to look)
The abstract follows below.
Some remarks: The paper is the journal version of our CSL'04 paper. It
became longer than expected because we took pains to prove everything
in full and to make the paper self-contained. This concerns in
particular the construction of the free *-autonomous category, which
was only sketched in the CSL paper. Since we avoided any kind of
hand-waving, the stuff should be accessible also to the beginner (in
both, proof theory and category theory)
Any comments are welcome.
Ciao,
Lutz
***********************************************************
Title: From Proof Nets to the Free *-Autonomous Category
Authors: Francois Lamarche and Lutz Strassburger
Abstract:
In the first part of this paper we present a theory of proof nets for
full multiplicative linear logic, including the two units. It
naturally extends the well-known theory of unit-free multiplicative
proof nets. A linking is no longer a set of axiom links but a tree in
which the axiom links are subtrees. These trees will be identified
according to an equivalence relation based on a simple form of graph
rewriting. We show the standard results of sequentialization and
strong normalization of cut elimination. In the second part of the
paper we show that the identifications enforced on proofs are such
that the class of two-conclusion proof nets defines the free
*-autonomous category.
