Logic in Computer Science (LICS 2005)

Paper: Constructing Free Boolean Categories (at LICS 2005)

Authors: Francois Lamarche 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 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{LamarcheStrassburge-ConstructingFreeBoo,
    author = 	 {Francois Lamarche and Lutz Strassburger},
    title = 	 {Constructing Free Boolean Categories},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {209--218},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }