Re: proof nets for multiplicative units

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.
>