{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T11:03:09Z","timestamp":1784804589309,"version":"3.55.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325914","type":"print"},{"value":"9783032325921","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\pi $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03c0<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -calculus as formulas. We provide correctness criterion, sequentialization procedure, and a proof translation algorithm.\n                  <\/jats:p>\n                  <jats:p>We show that proof nets provide a canonical representation of sequent calculus derivations modulo rule permutations.<\/jats:p>","DOI":"10.1007\/978-3-032-32592-1_4","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:21:33Z","timestamp":1784802093000},"page":"55-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proof Nets for\u00a0PiL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0425-2825","authenticated-orcid":false,"given":"Matteo","family":"Acclavio","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-9583-1017","authenticated-orcid":false,"given":"Giulia","family":"Manara","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Abrusci, V., Ruet, P.: Non-commutative logic I: the multiplicative fragment. Ann. Pure Appl. Logic 101(1), 29\u201364 (1999). https:\/\/doi.org\/10.1016\/S0168-0072(99)00014-7, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0168007299000147","DOI":"10.1016\/S0168-0072(99)00014-7"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Maieli, R.: Generalized connectives for multiplicative linear logic. In: Fern\u00e1ndez, M., Muscholl, A. (eds.) 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). LIPIcs, vol.\u00a0152, pp. 6:1\u20136:16. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.6, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/11649","DOI":"10.4230\/LIPIcs.CSL.2020.6"},{"key":"4_CR3","unstructured":"Acclavio, M., Manara, G.: Proof nets for PiL (full version) (2026). https:\/\/arxiv.org\/abs\/2605.14476"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-031-91118-7_2","volume-title":"Programming Languages and Systems","author":"M Acclavio","year":"2025","unstructured":"Acclavio, M., Manara, G., Montesi, F.: Formulas as processes, deadlock-freedom as choreographies. In: Vafeiadis, V. (ed.) ESOP 2025. LNCS, vol. 15694, pp. 23\u201355. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-91118-7_2"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Acclavio, M., Manara, G., Montesi, F.: Formulas as processes, deadlock-freedom as choreographies (extended version) (2025). https:\/\/arxiv.org\/abs\/2501.08928","DOI":"10.1007\/978-3-031-91118-7_2"},{"issue":"6","key":"4_CR6","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1017\/S0960129597002326","volume":"7","author":"G Bellin","year":"1997","unstructured":"Bellin, G.: Subnets of proof-nets in multiplicative linear logic with mix. Math. Struct. Comput. Sci. 7(6), 663\u2013669 (1997)","journal-title":"Math. Struct. Comput. Sci."},{"key":"4_CR7","unstructured":"Danos, V.: La Logique Lin\u00e9aire appliqu\u00e9e \u00e0 l\u2019\u00e9tude de divers processus de normalisation (principalement du Lambda-calcul). Ph.D. thesis, Universit\u00e9 Paris 7 (1990). http:\/\/www.theses.fr\/1990PA077188. Th\u00e8se de doctorat dirig\u00e9e par Girard, Jean-Yves Math\u00e9matiques Paris 7 1990"},{"issue":"3","key":"4_CR8","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). https:\/\/doi.org\/10.1007\/BF01622878","journal-title":"Arch. Math. Logic"},{"key":"4_CR9","unstructured":"Fiorillo, L., Osorio-Valencia, J., Saurin, A.: On correctness, sequentialization and interpolation. In: Talk at TLLA 2025: 17th International Workshop on the Theory and Applications of Linear Logic and Related Topics (2025). https:\/\/lipn.univ-paris13.fr\/TLLA\/2025\/abstracts\/14-fiorillo-osoriovalencia-saurin.pdf"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13(3\u20135), 341\u2013363 (2002). https:\/\/doi.org\/10.1007\/s001650200016","DOI":"10.1007\/s001650200016"},{"issue":"1","key":"4_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1\u2013101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR12","unstructured":"Girard, J.Y.: Proof-nets: the parallel syntax for proof-theory. In: Ursini, A., Agliano, P. (eds.) Logic and Algebra. Marcel Dekker, New York (1996)"},{"key":"4_CR13","first-page":"183","volume":"175","author":"JY Girard","year":"2000","unstructured":"Girard, J.Y.: On the meaning of logical rules II: multiplicatives and additives. NATO ASI Ser. F Comput. Syst. Sci. 175, 183\u2013212 (2000)","journal-title":"NATO ASI Ser. F Comput. Syst. Sci."},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Heijltjes, W.B., Hughes, D.J.D., Stra\u00dfburger, L.: Proof nets for first-order additive linear logic. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0131, pp. 22:1\u201322:22. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2019). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.22, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2019.22","DOI":"10.4230\/LIPIcs.FSCD.2019.22"},{"key":"4_CR15","unstructured":"Hughes, D.: First-order proofs without syntax. Berkeley Logic Colloquium (2014)"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Hughes, D., Heijltjes, W.: Conflict nets: efficient locally canonical mall proof nets. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science. p. 437\u2013446. LICS \u201916, Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2933575.2934559, https:\/\/doi.org\/10.1145\/2933575.2934559","DOI":"10.1145\/2933575.2934559"},{"key":"4_CR17","unstructured":"Hughes, D.J.D.: Abstract P-time proof nets for mall: Conflict nets (2008). https:\/\/arxiv.org\/abs\/0801.2421"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Hughes, D.J.D.: Unification nets: canonical proof net quantifiers. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, pp. 540\u2013549. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3209108.3209159, https:\/\/doi.org\/10.1145\/3209108.3209159","DOI":"10.1145\/3209108.3209159"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Hughes, D.J.D., Stra\u00dfburger, L., Wu, J.H.: Combinatorial proofs and decomposition theorems for first-order logic. In: 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201313 (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470579","DOI":"10.1109\/LICS52264.2021.9470579"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Hughes, D.J.D., Van Glabbeek, R.J.: Proof nets for unit-free multiplicative-additive linear logic. ACM Trans. Comput. Logic 6(4), 784\u2013842 (2005). https:\/\/doi.org\/10.1145\/1094622.1094629","DOI":"10.1145\/1094622.1094629"},{"key":"4_CR21","unstructured":"Martelli, A., Montanari, U.: Unification in linear time and space: a structured presentation. Istituto di Elaborazione della Informazione, Consiglio Nazionale delle Ricerche (1976)"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol.\u00a092. Springer, Cham (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Montesi, F.: Introduction to Choreographies. Cambridge University Press (2023). https:\/\/doi.org\/10.1017\/9781108981491","DOI":"10.1017\/9781108981491"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Nguy\u00ean, L.T.D., Stra\u00dfburger, L.: A system of interaction and structure III: the complexity of BV and pomset logic (2022). https:\/\/hal.inria.fr\/hal-03909547, working paper or preprint","DOI":"10.46298\/lmcs-19(4:25)2023"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Nguy\u00ean, L.T.D., Stra\u00dfburger, L.: BV and pomset logic are not the same. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0216, pp. 3:1\u20133:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2022.3, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2022\/15723","DOI":"10.4230\/LIPIcs.CSL.2022.3"},{"issue":"4","key":"4_CR26","doi-asserted-by":"publisher","first-page":"996","DOI":"10.1017\/S1755020323000138","volume":"17","author":"C Nicolai","year":"2024","unstructured":"Nicolai, C., Piazza, M., Tesi, M.: Non-contractive logics, paradoxes, and multiplicative quantifiers. Rev. Symb. Log. 17(4), 996\u20131017 (2024). https:\/\/doi.org\/10.1017\/S1755020323000138","journal-title":"Rev. Symb. Log."},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165\u2013193 (2003). https:\/\/doi.org\/10.1016\/S0890-5401(03)00138-X, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S089054010300138X. Theoretical Aspects of Computer Software (TACS 2001)","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"4_CR28","unstructured":"Retor\u00e9, C.: R\u00e9seaux et S\u00e9quents Ordonn\u00e9s. Ph.D. thesis, Universit\u00e9 Paris VII (1993)"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Retor\u00e9, C.: Pomset logic: the other approach to noncommutativity in logic. In: Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, pp. 299\u2013345 (2021)","DOI":"10.1007\/978-3-030-66545-6_9"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Retor\u00e9, C.: Handsome proof-nets: perfect matchings and cographs. Theoret. Comput. Sci. 294(3), 473\u2013488 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(01)00175-X, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S030439750100175X. Linear Logic","DOI":"10.1016\/S0304-3975(01)00175-X"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Saurin, A.: Interpolation as cut-introduction: on the computational content of craig-lyndon interpolation. In: Fern\u00e1ndez, M. (ed.) 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0337, pp. 32:1\u201332:21. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2025). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2025.32, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2025.32","DOI":"10.4230\/LIPIcs.FSCD.2025.32"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Tiu, A.F.: A system of interaction and structure II: the need for deep inference. 2(2), 1\u201324 (2006). https:\/\/doi.org\/10.2168\/LMCS-2(2:4)2006","DOI":"10.2168\/LMCS-2(2:4)2006"},{"issue":"1","key":"4_CR33","doi-asserted-by":"publisher","first-page":"41","DOI":"10.2307\/2274953","volume":"55","author":"DN Yetter","year":"1990","unstructured":"Yetter, D.N.: Quantales and (noncommutative) linear logic. J. Symb. Log. 55(1), 41\u201364 (1990). https:\/\/doi.org\/10.2307\/2274953","journal-title":"J. Symb. Log."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32592-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:21:37Z","timestamp":1784802097000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32592-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325914","9783032325921"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32592-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/ijcar","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}