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