[AM20] Matteo Acclavio and Roberto Maieli. Generalized Connectives for Multiplicative Linear Logic. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. doi:10.4230/LIPIcs.CSL.2020.6.

[APR05] Jean-Marc Andreoli, Gabriele Pulcini, and Paul Ruet. Permutative logic. In C.-H. Luke Ong, editor, Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 184–199. Springer, 2005. doi:10.1007/11538363_14.

[AR99] V. Michele Abrusci and Paul Ruet. Non-commutative logic I: the multiplicative fragment. Annals of Pure and Applied Logic, 101(1):29–64, 1999. doi:10.1016/S0168-0072(99)00014-7.

[ATS19] Andrea Aler Tubella and Lutz Straßburger. Introduction to Deep Inference. Lecture notes, August 2019. URL: https://hal.inria.fr/hal-02390267.

[Bas94] David A. Basin. A term equality problem equivalent to graph isomorphism. Information Processing Letters, 51(2):61–66, 1994. doi:10.1016/0020-0190(94)00084-0.

[BdGR97] Denis Béchet, Philippe de Groote, and Christian Retoré. A complete axiomatisation for the inclusion of series-parallel partial orders. In Hubert Comon, editor, Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings, volume 1232 of Lecture Notes in Computer Science, pages 230–240. Springer, 1997. doi:10.1007/3-540-62950-5_74.

[BG18] Jørgen Bang-Jensen and Gregory Z. Gutin, editors. Classes of Directed Graphs. Springer Monographs in Mathematics. Springer, 2018. doi:10.1007/978-3-319-71840-8.

[BGI$^+$14] Richard Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden, and Lutz Straßburger. A logical basis for quantum evolution and entanglement. In Claudia Casadio, Bob Coecke, Michael Moortgat, and Philip Scott, editors, Categories and Types in Logic, Language, and Physics – Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, volume 8222 of Lecture Notes in Computer Science, pages 90–107. Springer, 2014. doi:10.1007/978-3-642-54789-8_6.

[BPS12] Richard Blute, Prakash Panangaden, and Sergey Slavnov. Deep inference and probabilistic coherence spaces. Applied Categorical Structures, 20(3):209–228, 2012. doi:10.1007/s10485-010-9241-0.

[Bru02] Paola Bruscoli. A purely logical account of sequentiality in proof search. In Peter J. Stuckey, editor, Logic Programming, 18th International Conference, ICLP 2002, Copenhagen, Denmark, July 29 - August 1, 2002, Proceedings, volume 2401 of Lecture Notes in Computer Science, pages 302–316. Springer, 2002. doi:10.1007/3-540-45619-8_21.

[BT01] Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In Robert Nieuwenhuis and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings, volume 2250 of Lecture Notes in Computer Science, pages 347–361. Springer, 2001. doi:10.1007/3-540-45653-8_24.

[CDW20] Cameron Calk, Anupam Das, and Tim Waring. Beyond formulas-as-cographs: an extension of boolean logic to arbitrary graphs. CoRR, abs/2004.12941, 2020. arXiv:2004.12941.

[CLB81] Derek G. Corneil, H. Lerchs, and L. Stewart Burlingham. Complement reducible graphs. Discrete Applied Mathematics, 3(3):163–174, 1981. doi:10.1016/0166-218X(81)90013-5.

[CP06] Christophe Crespelle and Christophe Paul. Fully dynamic recognition algorithm and certificate for directed cographs. Discrete Applied Mathematics, 154(12):1722–1741, 2006. doi:10.1016/j.dam.2006.03.005.

[CR79] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36–50, 1979. doi:10.2307/2273702.

[DG04] Pietro Di Gianantonio. Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity. In Computer Science Logic, volume 3210, pages 130–144, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. doi:10.1007/978-3-540-30124-0_13.

[dP14] Valeria de Paiva. Linear logic model of state revisited. Logic Journal of the IGPL, 22(5):791–804, 2014. doi:10.1093/jigpal/jzu013.

[DR89] Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28(3):181–203, 1989. doi:10.1007/BF01622878.
[FR94] Arnaud Fleury and Christian Retoré. The mix rule. *Mathematical Structures in Computer Science*, 4(2):273-285, 1994. doi:10.1017/S0960129500000451.

[Gir87] Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50(1):1-101, January 1987. doi:10.1016/0304-3975(87)90045-4.

[Gir89] Jean-Yves Girard. Towards a geometry of interaction. In J. W. Gray and A. Scedrov, editors, *Categories in Computer Science and Logic*, volume 92 of *Contemporary Mathematics*, pages 69-108. American Mathematical Society, Providence, RI, 1989. *Proceedings of a Summer Research Conference held June 14-20, 1987*. doi:10.1090/conm/092/1003197.

[GLMM13] Laurent Gourvès, Adria Lyra, Carlos A. Martinhon, and Jérôme Monnot. Complexity of trails, paths and circuits in arc-colored digraphs. *Discrete Applied Mathematics*, 161(6):819-828, April 2013. doi:10.1016/j.dam.2012.10.025.

[GS01] Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the Calculus of Structures. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, and Laurent Fribourg, editors, *Computer Science Logic*, volume 2142, pages 54-68. Springer Berlin Heidelberg, Berlin, Heidelberg, 2001. doi:10.1007/3-540-44802-0_5.

[GS11] Alessio Guglielmi and Lutz Straßburger. A system of interaction and structure V: the exponentials and splitting. *Mathematical Structures in Computer Science*, 21(3):563-584, 2011. doi:10.1017/S096012951100003X.

[Gug99] Alessio Guglielmi. A calculus of order and interaction, 1999. Obsolete version of [Gug07]. URL: https://arxiv.org/abs/cs/9910023v1.

[Gug07] Alessio Guglielmi. A system of interaction and structure. *ACM Transactions on Computational Logic*, 8(1), January 2007. According to the author, the published version contains errors introduced by the editorial processing; the authoritative version is https://arxiv.org/abs/cs/9910023. doi:10.1145/1182613.1182614.

[Hor15] Ross Horne. The consistency and complexity of multiplicative additive system virtual. *Scientific Annals of Computer Science*, 25(2):245-316, 2015. doi:10.7561/SACS.2015.2.245.

[HT19] Ross Horne and Alwen Tiu. Constructing weak simulations from linear implications for processes with private names. *Mathematical Structures in Computer Science*, 29(8):1275-1308, 2019. doi:10.1017/S0960129518000452.

[HTAC19] Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. De Morgan Dual Nominal Quanti-fiers Modelling Private Names in Non-Commutative Logic. *ACM Transactions on Computational Logic*, 20(4):22:1-22:44, 2019. doi:10.1145/3325821.

[Hug04] Dominic J.D. Hughes. Deep inference proof theory equals categorical proof theory minus coherence. Unfinished draft, 2004. URL: http://boole.stanford.edu/~dominic/papers/di/di.pdf.

[Hug12] Dominic J.D. Hughes. Simple free star-autonomous categories and full coherence. *Journal of Pure and Applied Algebra*, 216(11):2386-2410, 2012. doi:10.1016/j.jpaa.2012.03.020.

[Kah04] Ozan Kahramanoğulları. System BV without the Equalities for Unit. In *Computer and Information Sciences - ISCIS 2004*, volume 3280, pages 986-995. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004. doi:10.1007/978-3-540-30182-0_99.

[Kah08] Ozan Kahramanoğulları. System BV is NP-complete. *Annals of Pure and Applied Logic*, 152(1):107-121, March 2008. doi:10.1016/j.apal.2007.11.005.

[Lam58] Joachim Lambek. The mathematics of sentence structure. *The American Mathematical Monthly*, 65(3):154-170, 1958. doi:10.2307/2310058.

[Mel18] Paul-André Mellès. Ribbon Tensorial Logic. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18*, pages 689-698, Oxford, United Kingdom, 2018. ACM Press. doi:10.1145/3209108.3209129.

[MR12] Richard Moot and Christian Retoré. *The Logic of Categorial Grammars*, volume 6850 of *Lecture Notes in Computer Science*. Springer, 2012. doi:10.1007/978-3-642-31555-8.

[Mö89] Rolf H. Möhring. Computationally tractable classes of ordered sets. In Ivan Rival, editor, *Algorithms and Order*, pages 105-193. Springer Netherlands, Dordrecht, 1989. doi:10.1007/978-94-009-2639-4_4.

[Ngu19] Lê Thành Dũng (Tito) Nguyễn. Constrained path-finding and structure from acyclicity. *CoRR*, abs/1901.07028, 2019. arXiv:1901.07028.
[FR94] Arnaud Fleury and Christian Retoré. The mix rule. *Mathematical Structures in Computer Science*, 4(2):273-285, 1994. doi:10.1017/S0960129500000451.

[Gir87] Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50(1):1-101, January 1987. doi:10.1016/0304-3975(87)90045-4.

[Gir89] Jean-Yves Girard. Towards a geometry of interaction. In J. W. Gray and A. Scedrov, editors, *Categories in Computer Science and Logic*, volume 92 of *Contemporary Mathematics*, pages 69-108. American Mathematical Society, Providence, RI, 1989. *Proceedings of a Summer Research Conference held June 14-20, 1987*. doi:10.1090/conm/092/1003197.

[GLMM13] Laurent Gourvès, Adria Lyra, Carlos A. Martinhon, and Jérôme Monnot. Complexity of trails, paths and circuits in arc-colored digraphs. *Discrete Applied Mathematics*, 161(6):819-828, April 2013. doi:10.1016/j.dam.2012.10.025.

[GS01] Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the Calculus of Structures. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, and Laurent Fribourg, editors, *Computer Science Logic*, volume 2142, pages 54-68. Springer Berlin Heidelberg, Berlin, Heidelberg, 2001. doi:10.1007/3-540-44802-0_5.

[GS11] Alessio Guglielmi and Lutz Straßburger. A system of interaction and structure V: the exponentials and splitting. *Mathematical Structures in Computer Science*, 21(3):563-584, 2011. doi:10.1017/S096012951100003X.

[Gug99] Alessio Guglielmi. A calculus of order and interaction, 1999. Obsolete version of [Gug07]. URL: https://arxiv.org/abs/cs/9910023v1.

[Gug07] Alessio Guglielmi. A system of interaction and structure. *ACM Transactions on Computational Logic*, 8(1), January 2007. According to the author, the published version contains errors introduced by the editorial processing; the authoritative version is https://arxiv.org/abs/cs/9910023. doi:10.1145/1182613.1182614.

[Hor15] Ross Horne. The consistency and complexity of multiplicative additive system virtual. *Scientific Annals of Computer Science*, 25(2):245-316, 2015. doi:10.7561/SACS.2015.2.245.

[HT19] Ross Horne and Alwen Tiu. Constructing weak simulations from linear implications for processes with private names. *Mathematical Structures in Computer Science*, 29(8):1275-1308, 2019. doi:10.1017/S0960129518000452.

[HTAC19] Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. De Morgan Dual Nominal Quanti-fiers Modelling Private Names in Non-Commutative Logic. *ACM Transactions on Computational Logic*, 20(4):22:1-22:44, 2019. doi:10.1145/3325821.

[Hug04] Dominic J.D. Hughes. Deep inference proof theory equals categorical proof theory minus coherence. Unfinished draft, 2004. URL: http://boole.stanford.edu/~dominic/papers/di/di.pdf.

[Hug12] Dominic J.D. Hughes. Simple free star-autonomous categories and full coherence. *Journal of Pure and Applied Algebra*, 216(11):2386-2410, 2012. doi:10.1016/j.jpaa.2012.03.020.

[Kah04] Ozan Kahramanoğulları. System BV without the Equalities for Unit. In *Computer and Information Sciences - ISCIS 2004*, volume 3280, pages 986-995. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004. doi:10.1007/978-3-540-30182-0_99.

[Kah08] Ozan Kahramanoğulları. System BV is NP-complete. *Annals of Pure and Applied Logic*, 152(1):107-121, March 2008. doi:10.1016/j.apal.2007.11.005.

[Lam58] Joachim Lambek. The mathematics of sentence structure. *The American Mathematical Monthly*, 65(3):154-170, 1958. doi:10.2307/2310058.

[Mel18] Paul-André Mellès. Ribbon Tensorial Logic. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18*, pages 689-698, Oxford, United Kingdom, 2018. ACM Press. doi:10.1145/3209108.3209129.

[MR12] Richard Moot and Christian Retoré. *The Logic of Categorial Grammars*, volume 6850 of *Lecture Notes in Computer Science*. Springer, 2012. doi:10.1007/978-3-642-31555-8.

[Mö89] Rolf H. Möhring. Computationally tractable classes of ordered sets. In Ivan Rival, editor, *Algorithms and Order*, pages 105-193. Springer Netherlands, Dordrecht, 1989. doi:10.1007/978-94-009-2639-4_4.

[Ngu19] Lê Thành Dũng (Tito) Nguyễn. Constrained path-finding and structure from acyclicity. *CoRR*, abs/1901.07028, 2019. arXiv:1901.07028.
[Ngu20] Lê Thành Dũng (Tito) Nguyễn. Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix. *Logical Methods in Computer Science*, Volume 16, Issue 1(27):27:1-27:31, February 2020. doi:10.23638/LMCS-16(1:27)2020.

[NP20] Lê Thành Dũng (Tito) Nguyễn and Cécilia Pradic. Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, *47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)*, volume 168 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 135:1–135:20, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2020.135.

[NS18] Lê Thành Dũng (Tito) Nguyễn and Thomas Seiller. Coherent interaction graphs. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, *Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018*, volume 292 of *EPTCS*, pages 104–117, 2018. doi:10.4204/EPTCS.292.6.

[NS22] Lê Thành Dũng (Tito) Nguyễn and Lutz Straßburger. BV and Pomset Logic Are Not the Same. In Florin Manea and Alex Simpson, editors, *30th EACSL Annual Conference on Computer Science Logic (CSL 2022)*, volume 216 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 32:1–32:17, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2022.32.

[OP99] Peter W. O'Hearn and David J. Pym. The logic of bunched implications. *Bulletin of Symbolic Logic*, 5(2):215–244, 1999. doi:10.2307/421090.

[Pag06] Michele Pagani. Acyclicity and coherence in multiplicative exponential linear logic. In Zoltán Ésik, editor, *Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings*, volume 4207 of *Lecture Notes in Computer Science*, pages 531–545. Springer, 2006. doi:10.1007/11874683_35.

[Pag12] Michele Pagani. Visible acyclic differential nets, Part I: Semantics. *Annals of Pure and Applied Logic*, 163(3):238–265, March 2012. doi:10.1016/j.apal.2011.09.001.

[Red93] Uday S. Reddy. A linear logic model of state, 1993. Unpublished note. URL: https://www.cs.bham.ac.uk/~udr/papers/state.full.pdf.

[Ret93] Christian Retoré. Réseaux et séquents ordonnés. PhD thesis, Université Paris VII, February 1993. URL: https://tel.archives-ouvertes.fr/tel-00585634.

[Ret97a] Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In *Typed Lambda Calculi and Applications*, volume 1210, pages 300–318. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. doi:10.1007/3-540-62688-3_43.

[Ret97b] Christian Retoré. A semantic characterisation of the correctness of a proof net. *Mathematical Structures in Computer Science*, 7(5):445–452, October 1997. doi:10.1017/S096012959700234X.

[Ret99a] Christian Retoré. Handsome proof-nets: R&B-graphs, perfect matchings and series-parallel graphs. Research Report 3652, INRIA, March 1999. URL: https://hal.inria.fr/inria-00073020.

[Ret99b] Christian Retoré. Pomset Logic as a Calculus of Directed Cographs. Research Report 3714, INRIA, June 1999. URL: https://hal.inria.fr/inria-00072953.

[Ret03] Christian Retoré. Handsome proof-nets: perfect matchings and cographs. *Theoretical Computer Science*, 294(3):473–488, February 2003. doi:10.1016/S0304-3975(01)00175-X.

[Ret21] Christian Retoré. Pomset Logic: The other approach to noncommutativity in logic. In Claudia Casadio and Philip J. Scott, editors, *Joachim Lambek: the interplay of mathematics, logic, and linguistics*, Outstanding Contributions to Logic, chapter 9, pages 299–346. Springer, 2021. doi:10.1007/978-3-030-66545-6_9.

[Rov16] Luca Roversi. A deep inference system with a self-dual binder which is complete for linear lambda calculus. *Journal of Logic and Computation*, 26(2):677–698, 2016. doi:10.1093/logcom/exu033.

[Rue00] Paul Ruet. Non-commutative logic II: sequent calculus and phase semantics. *Mathematical Structures in Computer Science*, 10(2):277–312, April 2000. doi:10.1017/S0960129599003084.

[SG11] Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: the exponentials and decomposition. *ACM Transactions on Computational Logic*, 12(4):23:1–23:39, 2011. doi:10.1145/1970398.1970399.

[SK22] Will Simmons and Aleks Kissinger. Higher-Order Causal Theories Are Models of BV-Logic. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, *47th International Symposium on*
[Ngu20] Lê Thành Dũng (Tito) Nguyễn. Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix. *Logical Methods in Computer Science*, Volume 16, Issue 1(27):27:1-27:31, February 2020. doi:10.23638/LMCS-16(1:27)2020.

[NP20] Lê Thành Dũng (Tito) Nguyễn and Cécilia Pradic. Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, *47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)*, volume 168 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 135:1–135:20, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2020.135.

[NS18] Lê Thành Dũng (Tito) Nguyễn and Thomas Seiller. Coherent interaction graphs. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, *Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018*, volume 292 of *EPTCS*, pages 104–117, 2018. doi:10.4204/EPTCS.292.6.

[NS22] Lê Thành Dũng (Tito) Nguyễn and Lutz Straßburger. BV and Pomset Logic Are Not the Same. In Florin Manea and Alex Simpson, editors, *30th EACSL Annual Conference on Computer Science Logic (CSL 2022)*, volume 216 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 32:1–32:17, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2022.32.

[OP99] Peter W. O'Hearn and David J. Pym. The logic of bunched implications. *Bulletin of Symbolic Logic*, 5(2):215–244, 1999. doi:10.2307/421090.

[Pag06] Michele Pagani. Acyclicity and coherence in multiplicative exponential linear logic. In Zoltán Ésik, editor, *Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings*, volume 4207 of *Lecture Notes in Computer Science*, pages 531–545. Springer, 2006. doi:10.1007/11874683_35.

[Pag12] Michele Pagani. Visible acyclic differential nets, Part I: Semantics. *Annals of Pure and Applied Logic*, 163(3):238–265, March 2012. doi:10.1016/j.apal.2011.09.001.

[Red93] Uday S. Reddy. A linear logic model of state, 1993. Unpublished note. URL: https://www.cs.bham.ac.uk/~udr/papers/state.full.pdf.

[Ret93] Christian Retoré. Réseaux et séquents ordonnés. PhD thesis, Université Paris VII, February 1993. URL: https://tel.archives-ouvertes.fr/tel-00585634.

[Ret97a] Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In *Typed Lambda Calculi and Applications*, volume 1210, pages 300–318. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. doi:10.1007/3-540-62688-3_43.

[Ret97b] Christian Retoré. A semantic characterisation of the correctness of a proof net. *Mathematical Structures in Computer Science*, 7(5):445–452, October 1997. doi:10.1017/S096012959700234X.

[Ret99a] Christian Retoré. Handsome proof-nets: R&B-graphs, perfect matchings and series-parallel graphs. Research Report 3652, INRIA, March 1999. URL: https://hal.inria.fr/inria-00073020.

[Ret99b] Christian Retoré. Pomset Logic as a Calculus of Directed Cographs. Research Report 3714, INRIA, June 1999. URL: https://hal.inria.fr/inria-00072953.

[Ret03] Christian Retoré. Handsome proof-nets: perfect matchings and cographs. *Theoretical Computer Science*, 294(3):473–488, February 2003. doi:10.1016/S0304-3975(01)00175-X.

[Ret21] Christian Retoré. Pomset Logic: The other approach to noncommutativity in logic. In Claudia Casadio and Philip J. Scott, editors, *Joachim Lambek: the interplay of mathematics, logic, and linguistics*, Outstanding Contributions to Logic, chapter 9, pages 299–346. Springer, 2021. doi:10.1007/978-3-030-66545-6_9.

[Rov16] Luca Roversi. A deep inference system with a self-dual binder which is complete for linear lambda calculus. *Journal of Logic and Computation*, 26(2):677–698, 2016. doi:10.1093/logcom/exu033.

[Rue00] Paul Ruet. Non-commutative logic II: sequent calculus and phase semantics. *Mathematical Structures in Computer Science*, 10(2):277–312, April 2000. doi:10.1017/S0960129599003084.

[SG11] Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: the exponentials and decomposition. *ACM Transactions on Computational Logic*, 12(4):23:1–23:39, 2011. doi:10.1145/1970398.1970399.

[SK22] Will Simmons and Aleks Kissinger. Higher-Order Causal Theories Are Models of BV-Logic. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, *47th International Symposium on*
*Mathematical Foundations of Computer Science (MFCS 2022)*, volume 241 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 80:1–80:14, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.MFCS.2022.80.

[Sla19] Sergey Slavnov. On noncommutative extensions of linear logic. *Logical Methods in Computer Science*, Volume 15, Issue 3, September 2019. doi:10.23638/LMCS-15(3:30)2019.

[Str03a] Lutz Straßburger. System NEL is undecidable. *Electronic Notes in Theoretical Computer Science*, 84:166–177, 2003. doi:10.1016/S1571-0661(04)80853-3.

[Str03b] Lutz Straßburger. *Linear Logic and Noncommutativity in the Calculus of Structures*. PhD Thesis, Technische Universität Dresden, 2003. URL: https://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf.

[Str12] Lutz Straßburger. Extension without cut. *Annals of Pure and Applied Logic*, 163(12):1995–2007, 2012. doi:10.1016/j.apal.2012.07.004.

[Tiu06] Alwen Tiu. A System of Interaction and Structure II: The Need for Deep Inference. *Logical Methods in Computer Science*, 2(2):4, April 2006. doi:10.2168/LMCS-2(2:4)2006.

[Tra08] Paolo Tranquilli. A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic. In Michael Kaminski and Simone Martini, editors, *Computer Science Logic*, volume 5213, pages 246–261. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008. doi:10.1007/978-3-540-87531-4_19.

[VTL82] Jacobo Valdes, Robert Endre Tarjan, and Eugene L. Lawler. The recognition of series parallel digraphs. *SIAM Journal on Computing*, 11(2):298–313, 1982. doi:10.1137/0211023.

[Wra76] Celia Wrathall. Complete sets and the polynomial-time hierarchy. *Theoretical Computer Science*, 3(1):23–33, October 1976. doi:10.1016/0304-3975(76)90062-1.

[Yet90] David N. Yetter. Quantales and (noncommutative) linear logic. *The Journal of Symbolic Logic*, 55(1):41–64, March 1990. doi:10.2307/2274953.

[ZG15] Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. *Logical Methods in Computer Science*, 11(3), 2015. doi:10.2168/LMCS-11(3:22)2015.
*Mathematical Foundations of Computer Science (MFCS 2022)*, volume 241 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 80:1–80:14, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.MFCS.2022.80.

[Sla19] Sergey Slavnov. On noncommutative extensions of linear logic. *Logical Methods in Computer Science*, Volume 15, Issue 3, September 2019. doi:10.23638/LMCS-15(3:30)2019.

[Str03a] Lutz Straßburger. System NEL is undecidable. *Electronic Notes in Theoretical Computer Science*, 84:166–177, 2003. doi:10.1016/S1571-0661(04)80853-3.

[Str03b] Lutz Straßburger. *Linear Logic and Noncommutativity in the Calculus of Structures*. PhD Thesis, Technische Universität Dresden, 2003. URL: https://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf.

[Str12] Lutz Straßburger. Extension without cut. *Annals of Pure and Applied Logic*, 163(12):1995–2007, 2012. doi:10.1016/j.apal.2012.07.004.

[Tiu06] Alwen Tiu. A System of Interaction and Structure II: The Need for Deep Inference. *Logical Methods in Computer Science*, 2(2):4, April 2006. doi:10.2168/LMCS-2(2:4)2006.

[Tra08] Paolo Tranquilli. A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic. In Michael Kaminski and Simone Martini, editors, *Computer Science Logic*, volume 5213, pages 246–261. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008. doi:10.1007/978-3-540-87531-4_19.

[VTL82] Jacobo Valdes, Robert Endre Tarjan, and Eugene L. Lawler. The recognition of series parallel digraphs. *SIAM Journal on Computing*, 11(2):298–313, 1982. doi:10.1137/0211023.

[Wra76] Celia Wrathall. Complete sets and the polynomial-time hierarchy. *Theoretical Computer Science*, 3(1):23–33, October 1976. doi:10.1016/0304-3975(76)90062-1.

[Yet90] David N. Yetter. Quantales and (noncommutative) linear logic. *The Journal of Symbolic Logic*, 55(1):41–64, March 1990. doi:10.2307/2274953.

[ZG15] Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. *Logical Methods in Computer Science*, 11(3), 2015. doi:10.2168/LMCS-11(3:22)2015.