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

]. K. Brü03a and . Brünnler, Atomic cut elimination for classical logic, CSL'03Brü03b] Kai Brünnler. Deep Inference and Symmetry in Classical Proofs, pp.86-97, 2003.

K. Brünnler and A. Tiu, A Local System for Classical Logic, LPAR'01, pp.347-361, 2001.
DOI : 10.1007/3-540-45653-8_24

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

A. Ciabattoni, N. Galatos, and K. Terui, From Axioms to Analytic Rules in Nonclassical Logics, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.229-240, 2008.
DOI : 10.1109/LICS.2008.39

A. Ciabattoni and R. Ramanayake, Structural Extensions of Display Calculi: A General Recipe, LNCS, vol.8071, pp.81-95, 2013.
DOI : 10.1007/978-3-642-39992-3_10

L. [. Ciabattoni, K. Straßburger, and . Terui, Expanding the Realm of Systematic Proof Theory, LNCS, vol.72, issue.3, pp.163-178, 2009.
DOI : 10.2178/jsl/1191333839
URL : https://hal.archives-ouvertes.fr/inria-00436420

T. [. Guglielmi, L. Gundersen, and . 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

]. T. Ghp13a, W. Gundersen, M. Heijltjes, ]. T. Parigotghp13b, W. Gundersen et al., Atomic lambdacalculus , a typed lambda-calculus with explicit sharing A proof of strong normalisation of the typed atomic lambda-calculus, LICS'13, pp.340-354, 2013.

S. Gimenez and G. Moser, The structure of interaction, LIPIcs, vol.23, pp.316-331, 2013.

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

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

]. N. Gue13 and . Guenot, Nested Deduction in Logical Foundations for Computation, 2013.

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

G. Mints, Interpolation theorems for intuitionistic predicate logic, Annals of Pure and Applied Logic, vol.113, issue.1-3, pp.225-242, 2001.
DOI : 10.1016/S0168-0072(01)00060-4

L. Straßburger and A. Guglielmi, A system of interaction and structure IV: The exponentials and decomposition, ACM Transactions on Computational Logic, vol.12, issue.4, p.23, 2011.

P. Schroeder-heister, Implications-as-Rules vs. Implications-as-Links: An Alternative Implication-Left Schema for the Sequent Calculus, Str03a] L. Straßburger. Linear Logic and Noncommutativity in the Calculus of Structures, pp.95-101, 2003.
DOI : 10.1007/s10992-010-9149-z

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

]. A. Tiu06 and . Tiu, A local system for intuitionistic logic, LPAR'06, pp.242-256, 2006.