EMIS ELibM Electronic Journals PUBLICATIONS DE L'INSTITUT MATHEMATIQUE (BEOGRAD) (N.S.)
Vol. 78(92), pp. 1–33 (2005)

Next Article

Contents of this Issue

Other Issues

ELibM Journals

ELibM Home

EMIS Home

Pick a mirror

 		 

COHERENCE OF Proof-Net CATEGORIES

Kosta Dosen and Zoran Petric

Matematicki institut SANU, Beograd, Serbia and Montenegro

Abstract: The notion of proof-net category defined in this paper is closely related to graphs implicit in proof nets for the multiplicative fragment without constant propositions of linear logic. Analogous graphs occur in Kelly's and Mac Lane's coherence theorem for symmetric monoidal closed categories. A coherence theorem with respect to these graphs is proved for proof-net categories. Such a coherence theorem is also proved in the presence of arrows corresponding to the mix principle of linear logic. The notion of proof-net category catches the unit free fragment of the notion of star-autonomous category, a special kind of symmetric monoidal closed category.

Keywords: generality of proofs; linear logic; mix; proof nets; linear distribution; dissociativity; categorial coherence; Kelly-Mac Lane graphs; Brauerian graphs; split equivalences; symmetric monoidal closed category; star-autonomous category

Classification (MSC2000): 03F07; 03F52; 18D10; 18D15; 19D23

Full text of the article: (for faster download, first choose a mirror)

Electronic fulltext finalized on: 2 Mar 2006. This page was last modified: 27 Oct 2006.

© 2006 Mathematical Institute of the Serbian Academy of Science and Arts
© 2006 ELibM and FIZ Karlsruhe / Zentralblatt MATH for the EMIS Electronic Edition