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

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

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.

A. Carbone, Interpolants, cut elimination and flow graphs for the propositional calculus, Annals of Pure and Applied Logic, vol.83, issue.3, pp.249-299, 1997.
DOI : 10.1016/S0168-0072(96)00019-X

A. Stephen, R. A. Cook, and . Reckhow, The relative efficiency of propositional proof systems, The Journal of Symbolic Logic, vol.44, issue.1, pp.36-50, 1979.

J. R. Cockett and R. A. Seely, Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories, Theory and Applications of Categories, vol.3, issue.5, pp.85-131, 1997.

J. R. Cockett and R. A. Seely, Weakly distributive categories, Journal of Pure and Applied Algebra, vol.114, issue.2, pp.133-173, 1997.
DOI : 10.1016/0022-4049(95)00160-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.7455

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

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

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 IEEE Symposium on Logic in Computer Science, 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, 2004.
DOI : 10.1016/j.jpaa.2005.03.016

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

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

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

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

A. Guglielmi, Deep inference and speed-up in proof search. Email to the frogs mailinglist on 2004-08-08, Gug04b] Alessio Guglielmi. Formalism A. note, 2004.

A. Guglielmihdp93, ]. J. Martin, E. Hyland, and V. De-paiva, Some news on subatomic logic. note Full intuitionistic linear logic (extended abstract), Annals of Pure and Applied Logic, vol.64, issue.3, pp.273-291, 1993.

R. Houston, D. Hughes, and A. Schalk, Modelling linear logic without units (preliminary results) Available at http://arxiv.org/abs, 2005.

W. A. Howard, The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

D. Hughes, Simple free star-autonomous categories and full coherence. preprint available at http://arxiv.org/abs/math.CT/0506521 Simple multiplicative proof nets with units, Hug05b] Dominic Hughes, 2005.
DOI : 10.1016/j.jpaa.2012.03.020
URL : http://arxiv.org/abs/math/0506521

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

Y. Lafont and . Logique, Catégories et Machines, 1988.

Y. Lafont, From proof nets to interaction nets, Advances in Linear Logic, pp.225-247, 1995.
DOI : 10.1017/CBO9780511629150.012

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, 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, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00113785

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

F. Lamarche and L. Straßburger, From Proof Nets to the Free *-Autonomous Category, Logical Methods in Computer Science, vol.2, issue.4, 2004.
DOI : 10.2168/LMCS-2(4:3)2006

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

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

S. Mac and L. , Natural associativity and commutativity, Rice University Studies, vol.49, pp.28-46, 1963.

S. Mac and L. , Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics, 1971.

R. Mckinley, New bureacracy/coherence. Email to the frogs mailinglist on 2005-06-03, 2005.

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

E. P. Robinsonsee89-]-r and . Seely, Proof Nets for Classical Logic, Linear logic, *-autonomous categories and cofree coalgebras. Contemporary Mathematics, pp.777-797, 1989.
DOI : 10.1093/logcom/13.5.777

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

L. Straßburger, From deep inference to proof nets, Structures and Deduction 2005 (Satellite Workshop of ICALP'05), 2005.

M. E. Szabo, Polycategories, Communications in Algebra, vol.3, issue.8, pp.663-689, 1975.
DOI : 10.1305/ndjfl/1093891297