M. Aigner and G. M. Ziegler, Proofs from THE BOOK (3, 2004.

]. H. Bar84 and . Barendregt, The lambda calculus : its syntax and semantics. Studies in logic and the foundations of mathematics, 1984.

M. Bagnol, A. Doumane, and A. Saurin, Analyse de dépendances et correction des réseaux de preuve, 25. Journées francophones des langages applicatifs, pp.159-174, 2014.

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

H. B. Curry and R. Feys, in Combinatory Logic, Combinatory Logic. Number, vol.1, 1958.

R. Cori and D. Lascar, Logique mathématique : Fonctions récursives , théorème de Gödel, théorie des ensembles, théorie des modèles, Axiomes, 1993.

A. Stephen, R. A. Cook, and . Reckhow, On the lengths of proofs in the propositional calculus (preliminary version), Proceedings of the 6th Annual ACM Symposium on Theory of Computing, pp.135-148, 1974.

J. W. Dawson, Why Prove it Again ? : Alternative Proofs in Mathematical Practice, 2015.
DOI : 10.1007/978-3-319-17368-9

K. Dosen, Abstract, Bulletin of Symbolic Logic, vol.53, issue.04, pp.477-503, 2003.
DOI : 10.2307/3072340

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

[. Ehrhard, A new correctness criterion for MLL proof nets, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pp.1-3810, 2014.
DOI : 10.1145/2603088.2603125

]. G. Fre79 and . Frege, Begriffsschrift, Eine Der Arithmetischen Nachgebildete Formelsprache Des Reinen Denkens, 1879.

]. G. Fre84 and . Frege, Die Grundlagen der Arithmetik : eine logisch mathematische Untersuchung über den Begriff der Zahl, p.1884

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

G. Gentzen, R. Feys, and J. Ladrière, Recherches sur la déduction logique : Traduction et commentaire, 1955.

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

T. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.47-58, 1990.
DOI : 10.1145/96709.96714

Y. Gurevich, What Is an Algorithm?, SOFSEM 2012 : Theory and Practice of Computer Science -38th Conference on Current Trends in Theory and Practice of Computer Science, ?pindler?v Mlýn, Czech Republic Proceedings, pp.31-42, 2012.
DOI : 10.1023/A:1015694932257

J. D. Dominic and . Hughes, Towards hilbert's 24 th problem : Combinatorial proof invariants : (preliminary version), Electr. Notes Theor. Comput. Sci, vol.165, pp.37-63, 2006.

G. Kreisel, J. L. Krivine, G. Kreisel, and J. L. Krivine, Elements of mathematical logic. (Model theory), 1967.

[. Kleene, Permutability of inferences in gentzens calculi lk and lj, In BULLETIN OF THE AMERICAN MATHEMATICAL SOCIETY, vol.57, pp.485-485, 1951.

]. G. Kre71 and . Kreisel, A survey of proof theory {II}, Proceedings of the Second Scandinavian Logic Symposium of Studies in Logic and the Foundations of Mathematics, pp.109-170, 1971.

G. Kreisel, Informal Rigour and Completeness Proofs, Problems in the Philosophy of Mathematics, pp.138-157, 1972.
DOI : 10.1016/S0049-237X(08)71525-8

Y. Lafont, Interaction nets, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.95-108, 1990.
DOI : 10.1145/96709.96718

Y. Lafont, From proof nets to interaction nets, pp.225-248, 1995.
DOI : 10.1017/CBO9780511629150.012

Y. Lafont, Interaction Combinators, Information and Computation, vol.137, issue.1, pp.69-101, 1997.
DOI : 10.1006/inco.1997.2643

URL : http://doi.org/10.1006/inco.1997.2643

J. Lambek, Cartesian closed categories and typed lambdacalculi Thirteenth Spring School of the LITP, Val d, Combinators and Functional Programming Languages Proceedings, pp.136-175, 1985.

]. D. Pra65 and . Prawitz, Natural deduction : a proof-theoretical study. Stockholm studies in philosophy, 1965.

D. Prawitz, Ideas and results in proof theory. north-holland publishing company, amsterdam and london, Journal of Symbolic Logic, vol.40, issue.6, pp.232-234, 1975.

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

L. Straßburger, Proof Nets and the Identity of Proofs, 2006.

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

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

A. Troelstra, Non-extensional equality, Fundamenta Mathematicae, vol.82, issue.4, pp.307-322, 1975.

]. F. Wid01 and . Widebäck, Identity of Proofs, Acta Universitatis Stockholmiensis. Almqvist & Wiksell International, 2001.