proof nets for MLL with units

Hello Frogs,

I would like to announce a paper by Francois and myself on proof net for 
multiplicative linear logic with units. 

A proof net should capture the essence of a proof such that two "morally 
identical" proofs are represented by the same object. Of course, the question 
is what is "morally identical". People usually consider here "up to trivial 
rule permutations in the sequent calculus". In this paper we do in principle 
the same. But there is one conceptual difference to Girards perception of 
what a proof net is. In Girards sense a proof net is a graph-like 
presentation of a sequent proof, where each rule gets a link assigned to it. 
This works well for MLL, badly for MALL and MELL, and not at all for the 
units, not to speak of classical logic. 

In our perception a proof net is a graph like thing containing the formula 
tree plus some "additional information". What this "additional information" 
is, depends on the logic in question. For MLL without units, it is simply the 
axiom links. If we add the units, we get more sophisticated linkings. This is 
what the paper is about.

-Lutz

-------------------

Authors: Lutz Strassburger and Francois Lamarche

Title:  On Proof Nets for Multiplicative Linear Logic with Units

Abstract:
  In this paper we present a theory of proof nets for 
  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.
  Furthermore, the identifications enforced on proofs are such that
  the proof nets, as they are presented here, form the arrows of the
  free (symmetric) *-autonomous category.

PDF available at:
http://www.loria.fr/~strassbu/papers/multPN.pdf