S. Abramsky, Computational interpretations of linear logic, Theoretical Computer Science, vol.111, issue.1-2, pp.3-57, 1993.
DOI : 10.1016/0304-3975(93)90181-R

M. Abadi, L. Cardelli, P. Curien, and J. Lévy, Explicit substitutions, POPL'90, pp.31-46, 1990.
DOI : 10.1145/96709.96712
URL : https://hal.archives-ouvertes.fr/inria-00075382

S. Alves and M. Florido, Weak linearization of the lambda calculus, Theoretical Computer Science, vol.342, issue.1, pp.79-103, 2005.
DOI : 10.1016/j.tcs.2005.06.005

B. Accattoli and D. Kesner, The Structural ??-Calculus, LNCS, vol.6247, issue.10, pp.381-395, 2010.
DOI : 10.1007/978-3-642-15205-4_30
URL : https://hal.archives-ouvertes.fr/hal-00528228

J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

M. Abrusci and P. Ruet, Non-commutative logic I: the multiplicative fragment, Annals of Pure and Applied Logic, vol.101, issue.1, pp.29-64, 1999.
DOI : 10.1016/S0168-0072(99)00014-7
URL : http://doi.org/10.1016/s0168-0072(99)00014-7

A. Asperti, Optimal reduction of functional expressions, PLILP'98, pp.427-428, 1998.
DOI : 10.1007/BFb0056630

A. Avron, The method of hypersequents in the proof theory of propositional non-classical logics, Logic: from foundations to applications: European logic colloquium, pp.1-32, 1996.

H. Barendregt, The Lambda Calculus: Its Syntax and Semantics, 1984.

G. Boudol, P. Curien, and C. Lavatelli, A semantics for lambda calculi with resources, Mathematical Structures in Computer Science, vol.9, issue.4, pp.437-482, 1999.
DOI : 10.1017/S0960129599002893

N. Belnap, Display logic, Journal of Philosophical Logic, vol.11, issue.4, pp.375-417, 1982.
DOI : 10.1007/BF00284976

P. Bruscoli and A. Guglielmi, A LINEAR LOGIC VIEW OF GAMMA STYLE COMPUTATIONS AS PROOF SEARCHES, Coordination Programming: Mechanisms, Models and Semantics, 1996.
DOI : 10.1142/9781848161023_0010

H. Barendregt and S. Ghilezan, Lambda terms for natural deduction, sequent calculus and cut elimination, Journal of Functional Programming, vol.10, issue.1, pp.121-134, 2000.
DOI : 10.1017/S0956796899003524

P. Bruscoli and A. Guglielmi, A Tutorial on Proof Theoretic Foundations of Logic Programming, LNCS, vol.2916, issue.03, pp.109-127, 2003.
DOI : 10.1007/978-3-540-24599-5_9

K. Brünnler and R. Mckinley, An Algorithmic Interpretation of a Deep Inference System, LPAR'08, pp.482-496, 2008.
DOI : 10.1007/978-3-540-89439-1_34

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

T. Brock-nannestad and C. Schürmann, Focused Natural Deduction, LNCS, vol.6397, issue.10, pp.157-171, 2010.
DOI : 10.1007/978-3-642-16242-8_12

G. Boudol, The ?-calculus with multiplicities (abstract), LNCS, vol.715, issue.93, pp.1-6, 1993.

R. Bloo and K. Rose, Preservation of strong normalisation in named ?calculi with explicit substitution and garbage collection, CSN'95, pp.62-72, 1995.

P. Bruscoli, A Purely Logical Account of Sequentiality in Proof Search, LNCS, vol.2401, issue.02, pp.302-316, 2002.
DOI : 10.1007/3-540-45619-8_21

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

K. Brünnler, Cut Elimination inside a Deep Inference System for Classical Predicate Logic, Studia Logica, vol.11, issue.1, pp.51-71, 2006.
DOI : 10.1007/s11225-006-6605-4

K. Brünnler, Deep Inference and Its Normal Form of Derivations, LNCS, vol.122, issue.1, pp.65-74, 2006.
DOI : 10.1007/978-3-642-66473-1

K. Brünnler, Locality for Classical Logic, Notre Dame Journal of Formal Logic, vol.47, issue.4, pp.557-580, 2006.
DOI : 10.1305/ndjfl/1168352668

K. Brünnler, Nested Sequents, 2010.

G. Bellin and P. Scott, On the ??-calculus and linear logic, Theoretical Computer Science, vol.135, issue.1, pp.11-65, 1994.
DOI : 10.1016/0304-3975(94)00104-9

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

K. Chaudhuri, Focusing Strategies in the Sequent Calculus of Synthetic Connectives, LPAR'08, pp.467-481, 2008.
DOI : 10.1007/978-3-540-89439-1_33

K. Chaudhuri, D. Miller, and A. Saurin, Canonical Sequent Proofs via Multi-Focusing, Fifth IFIP International Conference on Theoretical Computer Science, pp.383-396, 2008.
DOI : 10.1007/978-0-387-09680-3_26
URL : https://hal.archives-ouvertes.fr/hal-00527893

A. Church and J. B. Rosser, Some properties of conversion. Transactions of the, pp.472-482, 1936.

H. Curry, Functionality in combinatorial logic, Proceedings of National Academy of Sciences, pp.584-590, 1934.

H. Curry, The permutability of rules in the classical inferential calculus, The Journal of Symbolic Logic, vol.39, issue.04, pp.245-248, 1952.
DOI : 10.2307/2266612

. Nicolaas-de-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church- Rosser theorem, Indagationes Mathematicae, vol.34, pp.381-392, 1972.

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3
URL : http://doi.org/10.1016/0304-3975(82)90026-3

R. Dyckhoff and L. Pinto, Permutability of proofs in intuitionistic sequent calculi, Theoretical Computer Science, vol.212, issue.1-2, pp.141-155, 1999.
DOI : 10.1016/S0304-3975(98)00138-8

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992.
DOI : 10.1007/3-540-54487-9_58

T. Ehrhard and L. Regnier, The differential lambda-calculus, Theoretical Computer Science, vol.309, issue.1-3, pp.1-41, 2003.
DOI : 10.1016/S0304-3975(03)00392-X
URL : https://hal.archives-ouvertes.fr/hal-00150572

M. Fernández, I. Mackie, and F. Sinot, Lambda-Calculus with Director Strings, Applicable Algebra in Engineering, Communication and Computing, vol.11, issue.6, pp.393-437, 2005.
DOI : 10.1007/s00200-005-0169-9
URL : https://hal.archives-ouvertes.fr/inria-00133315

J. Gallier, Constructive logics Part I: A tutorial on proof systems and typed ??-calculi, Theoretical Computer Science, vol.110, issue.2, pp.249-339, 1993.
DOI : 10.1016/0304-3975(93)90011-H

R. Gandy, Proofs of strong normalisation, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

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

A. Guglielmi, T. Gundersen, and M. Parigot, A proof calculus which reduces syntactic bureaucracy, LIPIcs, vol.6, issue.10, pp.135-150, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00529301

A. Guglielmi, T. Gundersen, and L. Straßburger, Breaking Paths in Atomic Flows for Classical Logic, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.284-293, 2011.
DOI : 10.1109/LICS.2010.12
URL : https://hal.archives-ouvertes.fr/hal-00541076

J. Girard, Une extension de l'interpretation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types, Second Scandinavian Logic Symposium, pp.63-92, 1971.

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, Proof-nets : the parallel syntax for proof-theory, Logic and Algebra. M. Dekker, 1996.

J. Girard, Light linear logic. Information and Computation, pp.175-204, 1998.

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, 1989.

A. Guglielmi and L. Straßburger, A Non-commutative Extension of MELL, LPAR'02, pp.231-246, 2002.
DOI : 10.1007/3-540-36078-6_16

A. Guglielmi and L. Straßburger, A system of interaction and structure V: the exponentials and splitting, Mathematical Structures in Computer Science, vol.21, issue.03, 2009.
DOI : 10.1017/S096012951100003X
URL : https://hal.archives-ouvertes.fr/inria-00441254

A. Guglielmi and L. Straßburger, A system of interaction and structure IV: The exponentials and decomposition, ACM Transactions on Computational Logic, vol.12, issue.4, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00441214

A. Guglielmi and L. Straßburger, A system of interaction and structure V: the exponentials and splitting, Mathematical Structures in Computer Science, vol.21, issue.03, pp.563-584, 2011.
DOI : 10.1017/S096012951100003X
URL : https://hal.archives-ouvertes.fr/inria-00441254

A. Guglielmi, A calculus of order and interaction, 1999.

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

H. Herbelin, A ??-calculus structure isomorphic to Gentzen-style sequent calculus structure, CSL'94, pp.61-75, 1994.
DOI : 10.1007/BFb0022247
URL : https://hal.archives-ouvertes.fr/inria-00381525

J. S. Hodas and D. Miller, Logic Programming in a Fragment of Intuitionistic Linear Logic, Information and Computation, vol.110, issue.2, pp.327-365, 1994.
DOI : 10.1006/inco.1994.1036

W. 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, A minimal classical sequent calculus free of structural rules, Annals of Pure and Applied Logic, vol.161, issue.10, pp.1244-1253, 2010.
DOI : 10.1016/j.apal.2010.03.001

B. Jay and D. Kesner, First-class patterns, Journal of Functional Programming, vol.9, issue.02, pp.191-225, 2009.
DOI : 10.1016/j.tcs.2008.01.019
URL : https://hal.archives-ouvertes.fr/hal-00524750

R. [. Joachimski and . Matthes, Standardization and Confluence for a Lambda Calculus with Generalized Applications, LNCS, vol.1833, issue.00, pp.141-155, 2000.
DOI : 10.1007/10721975_10

]. O. Kah06 and . Kahramano?-gullar?, Nondeterminism and Language Design in Deep Inference, 2006.

R. Kashima, Cut-free sequent calculi for some tense logics, Studia Logica, vol.13, issue.1, pp.119-136, 1994.
DOI : 10.1007/BF01053026

]. D. Kes07 and . Kesner, The theory of calculi with explicit substitutions revisited, CSL'07, pp.238-252, 2007.

S. [. Kesner and . Lengrand, Extending the Explicit Substitution Paradigm, RTA'05, pp.407-422, 2005.
DOI : 10.1007/978-3-540-32033-3_30
URL : https://hal.archives-ouvertes.fr/hal-00148847

D. Kesner and S. Lengrand, Resource operators for the ?-calculus. Information and Computation, pp.419-473, 2007.

S. Kleene, On the interpretation of intuitionistic number theory, The Journal of Symbolic Logic, vol.3, issue.04, pp.109-124, 1945.
DOI : 10.1007/BF01565439

S. Kleene, Permutabilities of inferences in gentzen's calculi LK and LJ. Memoirs of the, pp.1-26, 1952.

J. W. Klop, Combinatory Reduction Systems, 1980.

D. Kesner and F. Renaud, A prismoid framework for languages with resources, Theoretical Computer Science, vol.412, issue.37, pp.4867-4892, 2011.
DOI : 10.1016/j.tcs.2011.01.026
URL : https://hal.archives-ouvertes.fr/hal-00625598

S. Kripke, Semantical Analysis of Intuitionistic Logic I, Formal Systems and Recursive Functions, pp.92-130, 1963.
DOI : 10.1016/S0049-237X(08)71685-9

R. Kennaway and R. Sleep, Director strings as combinators, ACM Transactions on Programming Languages and Systems, vol.10, issue.4, pp.602-626, 1988.
DOI : 10.1145/48022.48026

Y. Lafont, Soft linear logic and polynomial time, Theoretical Computer Science, vol.318, issue.1-2, pp.163-180, 2004.
DOI : 10.1016/j.tcs.2003.10.018
URL : http://doi.org/10.1016/j.tcs.2003.10.018

O. Laurent, Etude de la polarisation en logique, Thèse de doctorat, 2002.
URL : https://hal.archives-ouvertes.fr/tel-00007884

O. Laurent, A proof of the focalization property of linear logic, 2004.

P. Lescanne, From ?? to ??, a journey through calculi of explicit substitutions, POPL'94, pp.60-69, 1994.

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, CSL'07, pp.451-465, 2007.
DOI : 10.1007/978-3-540-74915-8_34
URL : https://hal.archives-ouvertes.fr/inria-00167231

D. [. Liang and . Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

J. Mccarthy, Recursive functions symbolic expressions and their computation by machine, Part I, Communications of the ACM, vol.3, issue.4, pp.184-195, 1960.
DOI : 10.1145/367177.367199

[. Melliès, Typed lambda-calculi with explicit substitutions may not terminate, TLCA'95, pp.328-334, 1995.

P. Melliès, Resource modalities in tensor logic, Annals of Pure and Applied Logic, vol.161, issue.5, pp.632-653, 2010.
DOI : 10.1016/j.apal.2009.07.018

]. R. Mil99 and . Milner, Communicating and Mobile Systems : The ?-calculus, 1999.

G. [. Miller, F. Nadathur, A. Pfenning, and . Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W
URL : http://doi.org/10.1016/0168-0072(91)90068-w

]. E. Mog89 and . Moggi, Computational ?-calculus and monads, LICS'89, pp.14-23, 1989.

D. Miller and A. Saurin, From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic, LNCS, vol.4646, issue.07, pp.405-419, 2007.
DOI : 10.1007/978-3-540-74915-8_31
URL : https://hal.archives-ouvertes.fr/hal-00527888

D. Maier and D. Warren, Computing With Logic: Logic Programming With Prolog, 1988.

M. Newman, On Theories with a Combinatorial Definition of "Equivalence", The Annals of Mathematics, vol.43, issue.2, pp.223-243, 1942.
DOI : 10.2307/1968867

S. Negri, J. V. , and P. , Structural Proof Theory, 2001.
DOI : 10.1017/CBO9780511527340
URL : https://hal.archives-ouvertes.fr/hal-01251230

E. Polonowski, Substitutions Explicites, Logique et Normalisation, 2004.

D. Prawitz, Natural Deduction: a proof-theoretical study, 1965.

B. Pierce and D. Turner, Local type inference, POPL'98, pp.252-265, 1998.
DOI : 10.1145/345099.345100

D. Pym, The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series. Kluwer, vol.26, 2002.
DOI : 10.1007/978-94-017-0091-7

F. Renaud, Les Ressources Explicites vues par la Théorie de la Réécriture, Thèse de doctorat, 2011.

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

J. Reynolds, Towards a theory of type structure, Symposium on Programming, pp.408-423, 1974.
DOI : 10.1007/3-540-06859-7_148

J. Reynolds, Theories of programming languages, 1998.
DOI : 10.1017/CBO9780511626364

L. Roversi, Linear Lambda Calculus and Deep Inference, LNCS, vol.2, issue.2, pp.184-197, 2011.
DOI : 10.1007/978-3-642-04081-8_7

]. D. San93 and . Sangiorgi, From ?-calculus to higher-order ?-calculus -and back, TAPSOFT'93, pp.151-166, 1993.

J. Espírito and S. , The ?-calculus and the unity of structural proof theory, Theory of Computing Systems, pp.963-994, 2009.

]. P. Sel07 and . Selinger, Lecture notes on the ?-calculus, 2007.

P. Schroeder-heister, Implications-as-Rules vs. Implications-as-Links: An Alternative Implication-Left Schema for the Sequent Calculus, Journal of Philosophical Logic, vol.49, issue.1, pp.95-101, 2011.
DOI : 10.1007/s10992-010-9149-z

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, A characterisation of medial as rewriting rule, LNCS, vol.4533, issue.07, pp.344-358, 2007.

M. Sørensen and P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, 2006.

A. Tiu, A Local System for Intuitionistic Logic, LNCS, vol.4246, issue.06, pp.242-256, 2006.
DOI : 10.1007/11916277_17

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. Tiu and D. Miller, A Proof Search Specification of the ??-Calculus, Third Workshop on the Foundations of Global Ubiquitous Computing, pp.79-101, 2004.
DOI : 10.1016/j.entcs.2005.05.006

A. Troelstra, Constructivism and proof theory, 2003.

A. Troelstra and H. Schwichtenberg, Basic Proof Theory, 1996.
DOI : 10.1017/CBO9781139168717

[. Viganò, Labelled Non-classical Logics, 2000.
DOI : 10.1007/978-1-4757-3208-5

D. Yetter, Quantales and (noncommutative) linear logic, The Journal of Symbolic Logic, vol.II, issue.01, pp.41-64, 1990.
DOI : 10.1017/S0305004100065403