Paper: Constructing Free Boolean Categories (at LICS 2005)

Authors: François Lamarche Lutz Straßburger

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 is different in several respects from the ones proposed recently. In particular everything is done from the start in a *-autonomous category and not in a weakly 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 a previously constructed category of proof nets 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 example with respect to units.

BibTeX

  @InProceedings{Straburger-ConstructingFreeBoo,
    author = 	 {François Lamarche and Lutz Straßburger},
    title = 	 {Constructing Free Boolean Categories},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {209--218},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }