proof nets for multiplicative units

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

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.