Proof nets for classical logic and Boolean categories

Hi Frogs,

We'd like to announce two papers.

The first one has already been announced here:

   Title: Naming Proofs in Classical Propositional Logic

   Authors: Francois Lamarche and Lutz Strassburger

It has been accepted at TLCA 2005 and the final version (as it will appear 
in the proceedings) is now available from our webpages:

http://www.ps.uni-sb.de/~lutz/
http://www.loria.fr/~lamarche/

Here is the abstract:

   We present a theory of proof denotations in classical propositional
   logic. The abstract definition is in terms of a semiring of weights,
   and two concrete instances are explored.  With the Boolean semiring
   we get a theory of classical proof nets, with a geometric
   correctness criterion, a sequentialization theorem, and a strongly
   normalizing cut-elimination procedure. This gives us a ``Boolean''
   category, which is not a poset. With the semiring of natural
   numbers, we obtain a sound semantics for classical logic, in which
   fewer proofs are identified. Though a ``real'' sequentialization
   theorem is missing, these proof nets have a grip on complexity
   issues.  In both cases the cut elimination procedure is closely
   related to its equivalent in the calculus of structures.


The second paper can be understood as a continuation of the first one:

   Title: Constructing free Boolean Categories

   Authors: Francois Lamarche and Lutz Strassburger

   Abstract:

   By Boolean category we mean something which is to a Boolean algebra
   what a category is to a poset. We propose an axiomatic system for
   Boolean categories, which differs in several respects from the one
   given very recently by F\"uhrmann and Pym. In particular everything
   is done from the start in a *-autonomous category and not a linear
   distributive one, which simplifies issues like the Mix rule.  An
   important axiom, which is introduced later, is a ``graphical''
   condition, which is closely related to denotational semantics and
   the Geometry of Interaction. Then we show that the proof net model
   presented in TLCA2005 is the free ``graphical'' Boolean category in
   our sense. This validates our categorical axiomatization with
   respect to a real-life example.  Another important aspect of this
   work is that we do not assume a-priori the existence of units in the
   *-autonomous categories we use. This has some retroactive interest
   for the semantics of linear logic, and is motivated by the
   properties of our TLCA proof nets with respect to units.


It has been submitted to LICS05 and is also available from our webpages. 
Since LICS allows only 10 pages, we also produced a longer version with 
all the proofs and some more discussion. This longer version is also 
available from our webpages.

Best wishes,
Lutz