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

W. Bibel, A deductive solution for plan generation, New Generation Computing, vol.14, issue.2, pp.115-132, 1986.
DOI : 10.1007/BF03037438

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

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.

C. Caleiro and R. Gonçalves, Equipollent logical systems, Birkhäuser, pp.99-111, 2005.
DOI : 10.1007/978-3-7643-8354-1_6

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

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

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

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.

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-00441254

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

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

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

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, Exploring the gap between linear and classical logic, 2006.
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, 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

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

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

D. Miller, A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-370, 1987.
DOI : 10.1007/BF00370646

[. Martin-löf, About Models for Intuitionistic Type Theories and the Notion of Definitional Equality, Proceedings of the Third Scandinavian Logic Symposium, pp.81-109, 1975.
DOI : 10.1016/S0049-237X(08)70727-4

S. Pollard, Homeomorphism and the Equivalence of Logical Systems, Notre Dame Journal of Formal Logic, vol.39, issue.3, pp.422-435, 1998.
DOI : 10.1305/ndjfl/1039182255

]. E. Pos41 and . Post, The Two-Valued Iterative Systems of Mathematical Logic, 1941.

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

F. J. Pelletier and A. Urquhart, Synonymous Logics, Journal of Philosophical Logic, vol.12, issue.3, pp.259-285, 2003.
DOI : 10.1023/A:1024248828122

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

F. Stouppa, The design of modal proof theories: the case of S5, 2004.

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.

L. Straßburger, Proof nets and the identity of proofs Lecture notes for ESSLLI'06 Available from https://hal.inria.fr/inria-00107260, 2006.

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