[TYPES] Paper Announcement: Free Boolean Categories

[Francois Lamarche]

We would like to make the following announcement.

Title:    Constructing free Boolean Categories

Authors:    Francois Lamache and Lutz Strassburber

This is an expanded version of our LICS’05 submission. Mistakes have 
been corrected and the relative emphasis of axioms has changed, but the 
claims are strictly identical.

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


This paper (as well as its predecessors) is available on the following 
pages:

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


François Lamarche and Lutz Strassburger