A. A. Tubella and A. Guglielmi, Subatomic Proof Systems: Splittable Systems, ACM Transactions on Computational Logic, vol.19, issue.1, pp.1-33, 2017.

A. A. Tubella, A. Guglielmi, and B. Ralph, Removing Cycles from Proofs, 26th EACSL Annual Conference on Computer Science Logic, vol.82, 2017.

A. Tubella, A study of normalisation through subatomic logic. Thesis, 2016.

P. Bruscoli and A. Guglielmi, On the proof complexity of deep inference, ACM Transactions on Computational Logic, vol.10, issue.2, pp.1-34, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00441211

C. Barrett and . Guglielmi, A Subatomic Proof System for Decision Trees, 2019.

P. Bruscoli, A purely logical account of sequentiality in proof search, Logic Programming, 18th International Conference, vol.2401, pp.302-316, 2002.

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

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

P. Bruscoli and L. Straßburger, On the length of medial-switch-mix derivations, Logic, Language, Information, and Computation -24th International Workshop, Proceedings, pp.68-79, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01635933

K. Brünnler and A. Tiu, A local system for classical logic, vol.2250, pp.347-361, 2001.

G. Bellin and J. Van-de-wiele, Subnets of proof-nets in MLL ?, Advances in Linear Logic, vol.222, pp.249-270, 1995.

A. Carbone, The cost of a cycle is a square, Journal of Symbolic Logic, vol.67, issue.1, pp.35-60, 2002.

K. Chaudhuri, N. Guenot, and L. Straßburger, The Focused Calculus of Structures, of Leibniz International Proceedings in Informatics (LIPIcs), vol.12, pp.159-173, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00772420

A. Das, On the proof complexity of cut-free bounded deep inference, Automated Reasoning with Analytic Tableaux and Related Methods -20th International Conference, vol.6793, pp.134-148, 2011.

A. Das, Complexity of deep inference via atomic flows, Computability in Europe, vol.7318, pp.139-150, 2012.

A. Das, Rewriting with linear inferences in propositional logic, 24th International Conference on Rewriting Techniques and Applications (RTA), volume 21 of Leibniz International Proceedings in Informatics (LIPIcs), pp.158-173, 2013.

A. Das, On the relative proof complexity of deep inference via atomic flows, Logical Methods in Computer Science, vol.11, issue.1, 2015.

V. Danos and L. Regnier, The structure of multiplicatives, Arch. Math. Log, vol.28, issue.3, pp.181-203, 1989.

A. Das and L. Straßburger, No complete linear term rewriting system for propositional logic, 26th International Conference on Rewriting Techniques and Applications, RTA 2015, vol.36, pp.127-142, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01236948

A. Das and L. Straßburger, On linear rewriting systems for boolean logic and some applications to proof theory, Logical Methods in Computer Science, vol.12, issue.4, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01422611

R. Duffin, Topology of series-parallel networks, Journal of Mathematical Analysis and Applications, vol.10, issue.2, pp.303-318, 1965.

G. Gentzen, Untersuchungenüber das logische Schließen, I. Mathematische Zeitschrift, vol.39, pp.176-210, 1935.

G. Gentzen, Untersuchungenüber das logische Schließen, II. Mathematische Zeitschrift, vol.39, pp.405-431, 1935.

A. Guglielmi and T. Gundersen, Normalisation control in deep inference via atomic flows, Logical Methods in Computer Science, vol.4, issue.9, pp.1-36, 2008.

A. Guglielmi, T. Gundersen, and M. Parigot, A Proof Calculus Which Reduces Syntactic Bureaucracy, 21st International Conference on Rewriting Techniques and Applications (RTA), vol.6, 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, Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, pp.284-293, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00541076

T. Gundersen, W. Heijltjes, and M. Parigot, A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19), vol.8312, pp.340-354, 2013.

T. Gundersen, W. Heijltjes, and M. Parigot, Atomic Lambda Calculus: {A} Typed Lambda-Calculus with Explicit Sharing, 28th Annual IEEE Symposium on Logic in Computer Science (LICS), pp.311-320, 2013.

J. Girard, Linear logic. Theoretical Computer Science, vol.50, pp.1-102, 1987.

J. Girard, Linear logic: its syntax and semantics, Advances in Linear Logic, pp.1-42, 1995.

K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, vol.38, pp.173-198, 1931.

A. Guglielmi and L. Straßburger, Non-commutativity and MELL in the calculus of structures, Computer Science Logic, vol.2142, pp.54-68, 2001.

A. Guglielmi and L. Straßburger, A non-commutative extension of MELL, Logic for Programming, vol.2514, pp.231-246, 2002.

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.3, pp.563-584, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00441254

N. Guenot and L. Straßburger, Symmetric Normalisation for Intuitionistic Logic, Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), vol.45, pp.1-10, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01092105

A. Guglielmi, Subatomic Logic, 2002.

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

T. Gundersen, A General View of Normalisation through Atomic Flows, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00441540

D. Hilbert and W. Ackermann, XXVII of Die Grundlehren der Mathematischen Wissenschaften. Verlag von Julius Springer, 1928.

F. He, The Atomic Lambda-Mu Calculus, 2018.

D. Hilbert, Die logischen Grundlagen der Mathematik, Mathematische Annalen, vol.88, pp.151-165, 1922.

R. Benjamin and . Horsfall, The Logic of Bunched Implications: {A} Memoir, 2006.

R. Horne, The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic, FSCD, 2019.

R. Horne and A. Tiu, Constructing weak simulations from linear implications for processes with private names, Mathematical Structures in Computer Science, vol.29, issue.8, pp.1275-1308, 2019.

R. Horne, A. Tiu, B. Aman, and G. Ciobanu, Private Names in Non-Commutative Logic, 27th International Conference on Concurrency Theory (CONCUR), vol.59, pp.1-31, 2016.

R. Horne, A. Tiu, B. Aman, and G. Ciobanu, De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic, ACM Trans. Comput. Logic, vol.20, issue.4, 2019.

D. Hughes, Proofs Without Syntax. Annals of Mathematics, vol.164, issue.3, pp.1065-1076, 2006.

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

Y. Lafont, Equational reasoning with 2-dimensional diagrams, LNCS, vol.909, pp.170-195, 1995.

F. Lamarche, Exploring the gap between linear and classical logic. Theory and Applications of Categories, vol.18, pp.473-535, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00113785

R. H. Möhring, Computationally tractable classes of ordered sets, Algorithms and Order, pp.105-194, 1989.

N. Novakovic and L. Straßburger, On the power of substitution in the calculus of structures, ACM Trans. Comput. Log, vol.16, issue.3, p.19, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00925707

D. Prawitz, Natural Deduction, A Proof-Theoretical Study. Almquist and Wiksell, 1965.

B. Ralph, A natural proof system for herbrand's theorem, Logical Foundations of Computer Science -International Symposium, vol.10703, pp.289-308, 2018.

B. Ralph, Modular Normalisation of Classical Proofs, 2019.

C. Retoré, Réseaux et Séquents Ordonnés, 1993.

C. Retoré, Handsome proof-nets: perfect matchings and cographs, Theoretical Computer Science, vol.294, issue.3, pp.473-488, 2003.

L. Roversi, Subatomic systems need not be subatomic, 2018.

L. Straßburger and A. Guglielmi, A system of interaction and structure IV: The exponentials and decomposition, ACM Trans. Comput. Log, vol.12, issue.4, p.23, 2011.

D. Sherratt, A lambda-calculus that achieves full laziness with spine duplication, 2019.

C. Stewart and P. Stouppa, A systematic proof theory for several modal logics, Advances in Modal Logic, vol.5, pp.309-333, 2005.

P. Stouppa, A deep inference system for the modal logic S5, Studia Logica, vol.85, issue.2, pp.199-214, 2007.

L. Straßburger, A local system for linear logic, Logic for Programming, vol.2514, pp.388-402, 2002.

L. Straßburger, A Local System for Linear Logic, Logic for Programming, vol.2514, pp.388-402, 2002.

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.

L. Straßburger, A characterisation of medial as rewriting rule, Term Rewriting and Applications, RTA'07, vol.4533, pp.344-358, 2007.

L. Straßburger, Deep inference for hybrid logic, International Workshop on Hybrid Logic, 2007.

L. Straßburger, On the axiomatisation of Boolean categories with and without medial. Theory and Applications of Categories, vol.18, pp.536-601, 2007.

L. Straßburger, Extension without cut, Annals of Pure and Applied Logic, vol.163, issue.12, 1995.

L. Straßburger, Combinatorial flows and their normalisation, 2nd International Conference on Formal Structures for Computation and Deduction, vol.84, pp.1-31, 2017.

A. Tiu, A local system for intuitionistic logic, Lecture Notes in Artificial Intelligence, vol.4246, pp.242-256, 2006.

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.

A. Sjerp-troelstra and H. Schwichtenberg, Basic Proof Theory, 2000.