M. Barr, *-Autonomous categories and linear logic, Mathematical Structures in Computer Science, vol.104, issue.02, pp.159-178, 1991.
DOI : 10.1016/0022-4049(89)90163-1

Z. [. Balteanu, R. Fiedorowicz, R. Schwänzl, and . Vogt, Iterated monoidal categories, Advances in Mathematics, vol.176, issue.2, pp.277-349, 2003.
DOI : 10.1016/S0001-8708(03)00065-3

URL : http://doi.org/10.1016/s0001-8708(03)00065-3

A. Blass, A game semantics for linear logic, Annals of Pure and Applied Logic, vol.56, issue.1-3, pp.183-220, 1992.
DOI : 10.1016/0168-0072(92)90073-9

R. Blute, Linear logic, coherence and dinaturality, Theoretical Computer Science, vol.115, issue.1, pp.3-41, 1993.
DOI : 10.1016/0304-3975(93)90053-V

URL : http://doi.org/10.1016/0304-3975(93)90053-v

P. [. Blute, S. Panangaden, and . Slavnov, Deep Inference and Probabilistic Coherence Spaces, Applied Categorical Structures, vol.2, issue.1:1, 2006.
DOI : 10.1007/s10485-010-9241-0

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.153.6952

K. Brünnler, Deep Inference and Symmetry in Classical Proofs, 2003.

K. Brünnler and A. Tiu, A Local System for Classical Logic, Lecture Notes in Artificial Intelligence, vol.2250, pp.347-361, 2001.
DOI : 10.1007/3-540-45653-8_24

A. Burroni, Higher-dimensional word problems with applications to equational logic, Theoretical Computer Science, vol.115, issue.1, pp.46-62, 1993.
DOI : 10.1016/0304-3975(93)90054-W

URL : http://doi.org/10.1016/0304-3975(93)90054-w

]. R. Cs97a, R. Cockett, and . Seely, Weakly distributive categories, J. Pure and Appl. Algebra, vol.173, pp.133-173, 1997.

R. Cockett and R. A. Seely, Proof theory for full intuitionistic linear logic, bilinear logic and mix categories, Theory and Appl. of Categories, vol.3, 1997.

K. Do?en and Z. Petri´cpetri´c, Proof-Theoretical Coherence, 2004.

V. De-paiva and A. Schalk, Poset-valued sets or how to build models for linear logics, Theoretical Computer Science, vol.315, issue.1, pp.83-107, 2004.

S. Eilenberg and G. M. Kelly, Closed Categories, Proceedings of the La Jolla Conference in Categorical Algebra, pp.421-562, 1966.
DOI : 10.1007/978-3-642-99902-4_22

A. Filinski, Declarative continuations and categorical duality Master's thesis, DIKU Report, vol.8911, 1989.
DOI : 10.1007/bfb0018355

]. T. Fox76 and . Fox, Coalgebras and cartesian categories, Communications in Algebra, vol.274, issue.7, pp.665-667, 1976.
DOI : 10.1080/00927877608822127

C. Führmann and D. Pym, On the geometry of interaction for classical logic, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., 2004.
DOI : 10.1109/LICS.2004.1319615

C. Führmann and D. Pym, On the geometry of interaction for classical logic (extended abstract), 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pp.211-220, 2004.

C. Führmann and D. Pym, Order-enriched categorical models of the classical sequent calculus, Journal of Pure and Applied Algebra, vol.204, issue.1, pp.21-68, 2005.
DOI : 10.1016/j.jpaa.2005.03.016

P. J. Freyd and D. Yetter, Braided compact closed categories with applications to low dimensional topology, Advances in Mathematics, vol.77, issue.2, pp.156-182, 1989.
DOI : 10.1016/0001-8708(89)90018-2

J. Girard, Geometry of Interaction 1: Interpretation of System F, Logic Colloquium 88, pp.221-260, 1989.
DOI : 10.1016/S0049-237X(08)70271-4

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types. Cambridge Tracts in Theoretical Computer Science, 1989.

. Th and . Griffin, A formulae-as-types notion of control, Principles of Programming Languages, pp.47-58, 1990.

A. Guglielmi, A system of interaction and structure, ACM Transactions on Computational Logic, vol.8, issue.1, 2007.
DOI : 10.1145/1182613.1182614

URL : https://hal.archives-ouvertes.fr/inria-00441214

J. Martin and E. Hyland, Abstract interpretation of proofs: Classical propositional calculus, Computer Science Logic, pp.6-21, 2004.

J. Lambek, Bilinear logic in algebra, and linguistics, Advances in Linear Logic, pp.43-59, 1994.
DOI : 10.1017/CBO9780511629150.003

[. Lamarche, Generalizing Coherence Spaces and Hypercoherences, Proceedings of MFPS 1995, 1995.
DOI : 10.1016/S1571-0661(04)00021-0

W. Lawvere, Metric spaces, generalized logic and closed categories Available as a TAC reprint, Rendiconti del Seminario Matematico e Fisico di, pp.135-166, 1973.

R. Loader, Totality and full completeness, Ninth Annual IEEE Symposium on Logic In Computer Science (LICS), pp.292-298, 1994.

J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic, volume 7 of Cambridge studies in advances mathematics, 1986.

F. Lamarche and L. Straßburger, Constructing Free Boolean Categories, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2005.
DOI : 10.1109/LICS.2005.13

URL : https://hal.archives-ouvertes.fr/hal-00012296

F. Lamarche and L. Straßburger, Naming proofs in classical logic, TLCA Proceedings, pp.246-261, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00012294

F. Lamarche and L. Straßsburger, From proof nets to the free * -automonous category, Logical Methods in Computer Science, vol.2, issue.4, 2006.

[. Mckinley, New bureaucracy/coherence. Email to the Frogs mailing list on 2005-06-03, 2005.

R. Mckinley, Virtual propositions: A sequent calculus for medial logic. Talk Given in Dresden, 2005.

R. Mckinley, Categorical Models of First-order Classical Proofs, 2006.

M. Nielsen, G. Plotkin, and G. Winskel, Petri nets, event structures and domains, part I, Theoretical Computer Science, vol.13, issue.1, pp.85-108, 1981.
DOI : 10.1016/0304-3975(81)90112-2

URL : http://doi.org/10.1016/0304-3975(81)90112-2

M. Nygaard and G. Winskel, Domain theory for concurrency, Theoretical Computer Science, vol.316, issue.1-3, pp.153-190, 2004.
DOI : 10.1016/j.tcs.2004.01.029

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.2078

C. L. Ong, A semantical view of classical proofs: Type-theoretic, categorical and denotational characterizations, Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS), pp.230-241, 1996.

M. Parigot, ?µ-calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning, LPAR 1992, pp.190-201, 1992.

E. P. Robinson, Proof Nets for Classical Logic, Journal of Logic and Computation, vol.13, issue.5, pp.777-797, 2003.
DOI : 10.1093/logcom/13.5.777

URL : http://logcom.oxfordjournals.org/cgi/content/short/13/5/777

R. Seely, Linear logic, *-autonomous categories and cofree coalgebras, Categories in Computer Science and Logic, 1989.
DOI : 10.1090/conm/092/1003210

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.6153

P. Selinger, Control categories and duality: on the categorical semantics of the lambda-mu calculus, Mathematical Structures in Computer Science, vol.11, issue.2, pp.207-260, 2001.
DOI : 10.1017/S096012950000311X

A. Simpson, Categorical completeness results for the simply-typed lambda-calculus, Proceedings of TLCA95, pp.414-427, 1995.
DOI : 10.1007/BFb0014068

T. Streicher and B. Reus, Classical logic, continuation semantics and abstract machines, Journal of Functional Programming, vol.8, issue.6, pp.543-572, 1998.
DOI : 10.1017/S0956796898003141

L. Straßburger, From deep inference to proof nets In Structures and Deduction ? The Quest for the Essence of Proofs, 2005.

L. Straßburger, On the axiomatization of Boolean categories, with or without Medial, Theory and Applications of Categories, vol.18, pp.471-533, 2007.

A. F. Tiu, A system of interaction and structure II: The need for deep inference. Logical Methods in Comp, Science, vol.2, issue.4, pp.1-24, 2006.

]. G. Wra75 and . Wraith, Lectures on elementary topoi, Model Theory and Topoi, pp.114-205, 1975.

&. Loria and . Inria-lorraine, Email: Francois.Lamarche@loria.fr This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at ftp://ftp.tac.mta.ca561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods, Projet Calligramme 615, rue du Jardin Botanique 54602 Villers

R. Blute, 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown (at) btinternet.com Aurelio Carboni, p.getzler

M. Hyland, U. Of-cambridge, :. M. Hyland@dpmms, and P. T. Johnstone, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk