{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:00:33Z","timestamp":1694620833371},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,5,22]],"date-time":"2018-05-22T00:00:00Z","timestamp":1526947200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s10817-018-9466-4","type":"journal-article","created":{"date-parts":[[2018,5,22]],"date-time":"2018-05-22T05:37:39Z","timestamp":1526967459000},"page":"911-939","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics"],"prefix":"10.1007","volume":"63","author":[{"given":"Matteo","family":"Acclavio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,22]]},"reference":[{"issue":"04","key":"9466_CR1","doi-asserted-by":"publisher","first-page":"1403","DOI":"10.2307\/2275485","volume":"56","author":"VM Abrusci","year":"1991","unstructured":"Abrusci, V.M.: Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic. J. Symb. Logic 56(04), 1403\u20131451 (1991)","journal-title":"J. Symb. Logic"},{"key":"9466_CR2","unstructured":"Acclavio, M. : A complete proof of coherence for symmetric monoidal categories using rewriting. arXiv:1606.01722 (2016)"},{"key":"9466_CR3","doi-asserted-by":"crossref","unstructured":"Acclavio, M.: Proof diagrams for multiplicative linear logic. arXiv:1606.09016 (2016)","DOI":"10.4204\/EPTCS.238.2"},{"key":"9466_CR4","doi-asserted-by":"crossref","unstructured":"John B.C., Lauda A.: A prehistory of n-categorical physics, pp. 13\u2013128. Cambridge University Press, Cambridge (2011)","DOI":"10.1017\/CBO9780511976971.003"},{"issue":"1","key":"9466_CR5","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0304-3975(93)90054-W","volume":"115","author":"A Burroni","year":"1993","unstructured":"Burroni, A.: Higher-dimensional word problems with applications to equational logic. Theor. Comput. Sci. 115(1), 43\u201362 (1993)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"9466_CR6","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BF01622878","volume":"28","author":"V Danos","year":"1989","unstructured":"Danos, V., Regnier, L.: The structure of multiplicatives. Arch. Math. Logic 28(3), 181\u2013203 (1989)","journal-title":"Arch. Math. Logic"},{"key":"9466_CR7","unstructured":"De Falco, L.T.: R\u00e9seaux, coh\u00e9rence et exp\u00e9riences obsessionnelles. Ph.D. thesis (2000)"},{"issue":"1","key":"9466_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1\u2013101 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"03","key":"9466_CR9","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J-Y Girard","year":"1991","unstructured":"Girard, J.-Y.: A new constructive logic: classic logic. Math. Struct. Comput. Sci. 1(03), 255\u2013296 (1991)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9466_CR10","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Linear logic: its syntax and semantics. London Mathematical Society Lecture Note Series, pp. 1\u201342 (1995)","DOI":"10.1017\/CBO9780511629150.002"},{"key":"9466_CR11","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Proof-nets: the parallel syntax for proof-theory. Lecture Notes, Pure and Applied Mathematics, pp. 97\u2013124 (1996)","DOI":"10.1201\/9780203748671-4"},{"issue":"1","key":"9466_CR12","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/S0304-3975(99)00299-6","volume":"254","author":"S Guerrini","year":"2001","unstructured":"Guerrini, S., Masini, A.: Parsing MELL proof nets. Theor. Comput. Sci. 254(1), 317\u2013335 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9466_CR13","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/j.jpaa.2005.10.011","volume":"207","author":"Y Guiraud","year":"2006","unstructured":"Guiraud, Y.: Termination orders for three-dimensional rewriting. J. Pure Appl. Algebra 207(2), 341\u2013371 (2006)","journal-title":"J. Pure Appl. Algebra"},{"key":"9466_CR14","unstructured":"Guiraud, Y: Catex Latex patch. https:\/\/www.irif.fr\/~guiraud\/catex\/s (2007)"},{"issue":"18","key":"9466_CR15","first-page":"420","volume":"22","author":"Y Guiraud","year":"2009","unstructured":"Guiraud, Y., Malbos, P.: Higher-dimensional categories with finite derivation type. Theory Appl. Categ. 22(18), 420\u2013478 (2009)","journal-title":"Theory Appl. Categ."},{"key":"9466_CR16","doi-asserted-by":"crossref","unstructured":"Heijltjes, W., Houston, R.: No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete. In: 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), p. 50. ACM, New York City (2014)","DOI":"10.1145\/2603088.2603126"},{"issue":"15","key":"9466_CR17","doi-asserted-by":"publisher","first-page":"3759","DOI":"10.1142\/S0217751X89001503","volume":"4","author":"M Jimbo","year":"1989","unstructured":"Jimbo, M.: Introduction to the Yang\u2013Baxter equation. Int. J. Mod. Phys. A 4(15), 3759\u20133777 (1989)","journal-title":"Int. J. Mod. Phys. A"},{"issue":"1","key":"9466_CR18","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0001-8708(91)90003-P","volume":"88","author":"Andr\u00e9 Joyal","year":"1991","unstructured":"Joyal, Andr\u00e9, Street, Ross: The geometry of tensor calculus I. Adv. Math. 88(1), 55\u2013112 (1991)","journal-title":"Adv. Math."},{"key":"9466_CR19","doi-asserted-by":"crossref","unstructured":"Lafont, Y: From proof nets to interaction nets. London Mathematical Society Lecture Note Series, pp. 225\u2013248 (1995)","DOI":"10.1017\/CBO9780511629150.012"},{"issue":"2","key":"9466_CR20","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0022-4049(03)00069-0","volume":"184","author":"Y Lafont","year":"2003","unstructured":"Lafont, Y.: Towards an algebraic theory of Boolean circuits. J. Pure Appl. Algebra 184(2), 257\u2013310 (2003)","journal-title":"J. Pure Appl. Algebra"},{"key":"9466_CR21","volume-title":"Categories for the Working Mathematician","author":"S Mac Lane","year":"2013","unstructured":"Mac Lane, S.: Categories for the Working Mathematician, vol. 5. Springer, Berlin (2013)"},{"key":"9466_CR22","first-page":"15","volume":"27","author":"P-A Mellies","year":"2009","unstructured":"Mellies, P.-A.: Categorical semantics of linear logic. Interact. Models Comput. Program Behav. 27, 15\u2013215 (2009)","journal-title":"Interact. Models Comput. Program Behav."},{"key":"9466_CR23","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-12821-9_4","volume-title":"New Structures for Physics","author":"P. Selinger","year":"2010","unstructured":"Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke B. (ed.) New structures for physics. Lecture notes in Physics, vol 813, pp. 289\u2013355. Springer, Berlin (2010)"},{"key":"9466_CR24","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-30124-0_14","volume-title":"Computer Science Logic","author":"Lutz Stra\u00dfburger","year":"2004","unstructured":"Stra\u00dfburger, L., Lamarche, F.: On proof nets for multiplicative linear logic with units. In: International Workshop on Computer Science Logic, pp. 145\u2013159. Springer, Berlin (2004)"},{"issue":"2","key":"9466_CR25","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0022-4049(76)90013-X","volume":"8","author":"R Street","year":"1976","unstructured":"Street, R.: Limits indexed by category-valued 2-functors. J. Pure Appl. Algebra 8(2), 149\u2013181 (1976)","journal-title":"J. Pure Appl. Algebra"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9466-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9466-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9466-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T23:58:03Z","timestamp":1661299083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9466-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,22]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["9466"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9466-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,22]]},"assertion":[{"value":"24 April 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 May 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 May 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}