B. Peter and . Andrews, Refutations by matings, IEEE Transactions on Computers, issue.25, pp.801-807, 1976.

V. M. , A. , and P. Ruet, Non-commutative logic I: The multiplicative fragment, Annals of Pure and Applied Logic, vol.101, pp.29-64, 2000.

M. Barr, *-Autonomous Categories, Lecture Notes in Mathematics, vol.752, 1979.
DOI : 10.1007/BFb0064579

R. Blute, R. Cockett, R. Seely, and T. Trimble, Natural deduction and coherence for weakly distributive categories, Journal of Pure and Applied Algebra, vol.113, issue.3, pp.229-296, 1996.
DOI : 10.1016/0022-4049(95)00159-X
URL : http://doi.org/10.1016/0022-4049(95)00159-x

W. Bibel, On Matrices with Connections, Journal of the ACM, vol.28, issue.4, pp.633-645, 1981.
DOI : 10.1145/322276.322277

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

G. Boolos, Don't eliminate cut, Journal of Philosophical Logic, vol.13, issue.4, pp.373-378, 1984.
DOI : 10.1007/BF00247711

K. Brünnler, Deep Inference and Symmetry for 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

R. Samuel and . Buss, The undecidability of k-provability. Annals of Pure and Applied Logic, pp.72-102, 1991.

G. Bellin and J. Van-de-wiele, Subnets of proof-nets in MLL ?, Advances in Linear Logic, pp.249-270, 1995.

T. Coquand and G. P. Huet, The calculus of constructions. Information and Computation, pp.95-120, 1988.
URL : https://hal.archives-ouvertes.fr/inria-00076024

[. Danos, La logique linéaire appliquéè a l'´ etude de divers processus de normalisation (principalement du ?-calcul), Thèse de Doctorat, 1990.

P. Di and G. , Structures for multiplicative cyclic linear logic: Deepness vs cyclicity, Computer Science Logic, pp.130-144, 2004.

H. Devarajan, D. Hughes, G. Plotkin, and V. R. Pratt, Full completeness of the multiplicative linear logic of Chu spaces, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999.
DOI : 10.1109/LICS.1999.782619

[. Do?en, Identity of proofs based on normalization and generality. The Bulletin of Symbolic Logic, pp.477-503, 2003.

[. Do?en and Z. Petri´cpetri´c, Proof-net categories. preprint, Mathematical Institute, 2005.

V. Danos and L. Regnier, The structure of multiplicatives, Archive for Mathematical Logic, vol.28, issue.3, pp.181-203, 1989.
DOI : 10.1007/BF01622878

S. Eilenberg and G. M. Kelly, A generalization of the functorial calculus, Journal of Algebra, vol.3, issue.3, pp.366-375, 1966.
DOI : 10.1016/0021-8693(66)90006-8

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, 2004.
DOI : 10.1016/j.jpaa.2005.03.016

A. Fleury and C. Retoré, The mix rule, Mathematical Structures in Computer Science, vol.28, issue.02, pp.273-285, 1994.
DOI : 10.1016/0304-3975(93)90181-R

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1934.
DOI : 10.1007/BF01201353

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. II, Mathematische Zeitschrift, vol.39, issue.1, pp.405-431, 1935.
DOI : 10.1007/BF01201363

J. Girard, Interprétation fonctionelle etéliminationetélimination des coupures de l'arithmétique d'ordre supérieur, 1972.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

[. 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

[. Girard, Proof-nets : the parallel syntax for proof-theory, Logic and Algebra. Marcel Dekker, 1996.

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

A. Guglielmi and L. Straßburger, Non-commutativity and MELL in the Calculus of Structures, LNCS, vol.2142, pp.54-68, 2001.
DOI : 10.1007/3-540-44802-0_5

A. Guglielmi and L. Straßburger, A non-commutative extension of multiplicative exponential linear logic, 2002.

S. Guerrini, Correctness of multiplicative proof nets is linear, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.454-463, 1999.
DOI : 10.1109/LICS.1999.782640

A. Guglielmi, A system of interaction and structure, ACM Transactions on Computational Logic, vol.8, issue.1, 2002.
DOI : 10.1145/1182613.1182614
URL : https://hal.archives-ouvertes.fr/inria-00441214

[. Houston, D. Hughes, and A. Schalk, Modelling linear logic without units (preliminary results). Preprint, 2005.

M. Horbach, Proof nets for intuitionistic logic, 2006.

D. Hughes, Deep inderence proof theory equals categorical proof theory minus coherence, 2004.

D. Hughes, Simple free star-autonomous categories and full coherence, Journal of Pure and Applied Algebra, vol.216, issue.11, 2005.
DOI : 10.1016/j.jpaa.2012.03.020
URL : http://arxiv.org/abs/math/0506521

[. Hughes, Simple multiplicative proof nets with units. Preprint, available at http://arxiv.org/abs/math, CT/0507003, 2005.

D. Hughes and R. Van-glabbeek, Proof nets for unit-free multiplicative-additive linear logic, 18th IEEE Symposium on Logic in Computer Science (LICS 2003), pp.1-10, 2003.
DOI : 10.1145/1094622.1094629

[. Joinet, Une preuve combinatoire de forte normalisation (du fragment multiplicatif et exponentiel) des réseaux de preuves pour la logique linéaire (PN1), Completeness of mll proof nets w.r.t. weak distributivity, 1992.

G. Maxwell, K. , and S. M. Lane, Coherence in closed categories, Journal of Pure and Applied Algebra, vol.1, pp.97-140, 1971.

[. Lafont, The linear abstract machine, Theoretical Computer Science, vol.59, issue.1-2, pp.157-180, 1988.
DOI : 10.1016/0304-3975(88)90100-4
URL : http://doi.org/10.1016/0304-3975(88)90100-4

[. Lafont, From proof nets to interaction nets, Advances in Linear Logic, pp.225-247, 1995.
DOI : 10.1017/CBO9780511629150.012
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.2755

J. Lambek, The Mathematics of Sentence Structure, The American Mathematical Monthly, vol.65, issue.3, pp.154-169, 1958.
DOI : 10.2307/2310058

J. Lambek, Deductive systems and categories, Mathematical Systems Theory, vol.49, issue.4, pp.287-318, 1968.
DOI : 10.1007/BF01703261

J. Lambek, Deductive systems and categories II. Standard constructions and closed categories, Lecture Notes in Mathematics, vol.260, pp.76-122, 1969.
DOI : 10.1007/BFb0079385

F. Lamarche, Proof nets for intuitionistic linear logic I: Essential nets, 1994.

F. Lamarche, Games semantics for full propositional linear logic, Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pp.464-473, 1995.
DOI : 10.1109/LICS.1995.523280

F. Lamarche, On the algebra of structural contexts, Accepted at Mathematical Structures in Computer Science, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00099461

F. Lamarche, Exploring the gap between linear and classical logic, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00113785

O. Laurent, Polarized Proof-Nets: Proof-Nets for LC, Typed Lambda Calculi and Applications, pp.213-227, 1999.
DOI : 10.1007/3-540-48959-2_16
URL : https://hal.archives-ouvertes.fr/hal-00009136

O. Laurent, Polarized proof-nets and ????-calculus, Theoretical Computer Science, vol.290, issue.1, pp.161-188, 2003.
DOI : 10.1016/S0304-3975(01)00297-3
URL : https://hal.archives-ouvertes.fr/hal-00009114

[. Lamarche and C. Retoré, Proof nets for the Lambek-calculus ? an overview, Proceedings of the Third Roma Workshop " Proofs and Linguistic Categories, pp.241-262, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00098442

J. Lambek and P. J. Scott, Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics, 1986.

[. Lamarche and L. Straßburger, Constructing Free Boolean Categories, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.209-218, 2005.
DOI : 10.1109/LICS.2005.13
URL : https://hal.archives-ouvertes.fr/hal-00012296

[. Lamarche and L. Straßburger, Naming Proofs in Classical Propositional Logic, Typed Lambda Calculi and Applications, pp.246-261, 2005.
DOI : 10.1007/11417170_19
URL : https://hal.archives-ouvertes.fr/hal-00012294

[. Lamarche and L. Straßburger, From Proof Nets to the Free *-Autonomous Category, Logical Methods in Computer Science, vol.2, issue.4, pp.1-44, 2006.
DOI : 10.2168/LMCS-2(4:3)2006
URL : http://arxiv.org/abs/cs/0605054

[. Lane, Natural Associativity and Commutativity, Rice University Studies, vol.49, pp.28-46, 1963.
DOI : 10.1007/978-1-4615-7831-4_19
URL : http://hdl.handle.net/1911/62865

[. Lane, Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics, 1971.

R. Mckinley, Classical categories and deep inference, Structures and Deduction 2005 (Satellite Workshop of ICALP'05), 2005.

R. Moot, Proof Nets for Linguistic Analysis, 2002.

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

D. Prawitz, Natural Deduction, A Proof-Theoretical Study. Almquist and Wiksell, 1965.

D. Prawitz, Ideas and Results in Proof Theory, Proceedings of the Second Scandinavian Logic Symposium, pp.235-307, 1971.
DOI : 10.1016/S0049-237X(08)70849-8

Q. Puite, Sequents and Link Graphs, 2001.

[. Retoré, Réseaux et Séquents Ordonnés, Thèse de Doctorat, spécialité mathématiques, 1993.

[. Retoré, Pomset logic: A non-commutative extension of classical linear logic, Typed Lambda Calculus and Applications, TLCA'97, pp.300-318, 1997.
DOI : 10.1007/3-540-62688-3_43

C. Retoré, Handsome proof-nets: R&B-graphs, perfect matchings and series-parallel graphs, 1999.

C. Retoré, Pomset logic as a calculus of directed cographs, Dynamic Perspectives in Logic and Linguistics, pp.221-247, 1999.

[. Retoré, Handsome proof-nets: perfect matchings and cographs, Theoretical Computer Science, vol.294, issue.3, pp.473-488, 2003.
DOI : 10.1016/S0304-3975(01)00175-X

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. See89 and . Seely, Linear logic, *-autonomous categories and cofree coalgebras, Contemporary Mathematics, vol.92, 1989.

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

L. Straßburger and F. Lamarche, On Proof Nets for Multiplicative Linear Logic with Units
DOI : 10.1007/978-3-540-30124-0_14

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, A local system for linear logic, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002, pp.388-402, 2002.

L. Straßburger, Linear Logic and Noncommutativity in the Calculus of Structures, 2003.

L. Straßburger, MELL in the calculus of structures, Theoretical Computer Science, vol.309, issue.1-3, pp.213-285, 2003.
DOI : 10.1016/S0304-3975(03)00240-8

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 axiomatisation of Boolean categories with and without medial, 2005.

H. Thielecke, Categorical Structure of Continuation Passing Style, 1997.

R. Thiele, Hilbert's Twenty-Fourth Problem, The American Mathematical Monthly, vol.110, issue.1, pp.1-24, 2003.
DOI : 10.2307/3072340

A. Tiu, Properties of a Logical System in the Calculus of Structures, 2001.

A. Tiu, A System of Interaction and Structure II: The Need for Deep Inference, Logical Methods in Computer Science, vol.2, issue.2, pp.1-24, 2006.
DOI : 10.2168/LMCS-2(2:4)2006

A. Sjerp, T. , and H. Schwichtenberg, Basic Proof Theory, 2000.

N. David and . Yetter, Quantales and (noncommutative) linear logic, Journal of Symbolic Logic, vol.55, issue.1, pp.41-64, 1990.

I. Unité-de-recherche, . Lorraine, . Loria, and . Technopôle-de-nancy, Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-l` es-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche INRIA Rocquencourt, Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche INRIA Sophia Antipolis : 2004, route des Lucioles -BP 93 -06902 Sophia Antipolis Cedex

I. Editeur and . De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399