{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T17:28:14Z","timestamp":1778520494182,"version":"3.51.4"},"publisher-location":"Cham","reference-count":96,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031911170","type":"print"},{"value":"9783031911187","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We introduce a novel approach to studying properties of processes in the <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>-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free <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>-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the <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>-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite <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>-calculus processes composed in parallel at the top level can be faithfully represented by a choreography.<\/jats:p>\n          <jats:p>With these results, we show how the computation-as-derivation paradigm extends the reach of logical methods for the study of concurrency, by bridging gaps between logic, the expressiveness of the <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>-calculus, and the expressiveness of choreographic languages.<\/jats:p>","DOI":"10.1007\/978-3-031-91118-7_2","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:04Z","timestamp":1746001024000},"page":"23-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formulas as Processes, Deadlock-Freedom as Choreographies"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0425-2825","authenticated-orcid":false,"given":"Matteo","family":"Acclavio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-9583-1017","authenticated-orcid":false,"given":"Giulia","family":"Manara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4666-901X","authenticated-orcid":false,"given":"Fabrizio","family":"Montesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"2_CR1","unstructured":"Abramsky, S.: Proofs as processes. In: Selected Papers of the Conference on Meeting on the Mathematical Foundations of Programming Semantics, Part I: Linear Logic: Linear Logic. pp.\u00a05\u20139. MFPS \u201992, Elsevier Science Publishers B. V., NLD (1992)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Acclavio, M.: Sequent systems on undirected graphs. In: Benzm\u00fcller, C., Heule, M.J., Schmidt, R.A. (eds.) Automated Reasoning. pp. 216\u2013236. Springer Nature Switzerland, Cham (2024)","DOI":"10.1007\/978-3-031-63501-4_12"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Curzi, G., Guerrieri, G.: Infinitary cut-elimination via finite approximations. CoRR abs\/2308.07789 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2308.07789, https:\/\/doi.org\/10.48550\/arXiv.2308.07789","DOI":"10.48550\/ARXIV.2308.07789"},{"key":"2_CR4","unstructured":"Acclavio, M., Curzi, G., Guerrieri, G.: Infinitary cut-elimination via finite approximations (extended version) (2024), https:\/\/arxiv.org\/abs\/2308.07789"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Horne, R., Mauw, S., Stra\u00dfburger, L.: A Graphical Proof Theory of Logical Time. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0228, pp. 22:1\u201322:25. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2022.22, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2022.22","DOI":"10.4230\/LIPIcs.FSCD.2022.22"},{"key":"2_CR6","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). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0152, pp. 6:1\u20136:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.6, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CSL.2020.6","DOI":"10.4230\/LIPIcs.CSL.2020.6"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Maieli, R.: Logic programming with multiplicative structures. CoRR abs\/2403.03032 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2403.03032, https:\/\/doi.org\/10.48550\/arXiv.2403.03032","DOI":"10.48550\/ARXIV.2403.03032"},{"key":"2_CR8","unstructured":"Acclavio, M., Manara, G.: Proofs as execution trees for the $$\\pi $$-calculus (2024), https:\/\/arxiv.org\/abs\/2411.08847"},{"key":"2_CR9","unstructured":"Acclavio, M., Manara, G., Montesi, F.: Formulas as processes, deadlock-freedom as choreographies (extended version) (2025), https:\/\/arxiv.org\/abs\/2501.08928"},{"key":"2_CR10","unstructured":"Acclavio, M., Montesi, F., Peressotti, M.: On propositional dynamic logic and concurrency (2024)"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Andreoli, J.M.: Focussing and proof construction. Annals of Pure and Applied Logic 107(1), 131\u2013163 (2001). https:\/\/doi.org\/10.1016\/S0168-0072(00)00032-4, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0168007200000324","DOI":"10.1016\/S0168-0072(00)00032-4"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Andreoli, J.M.: Focussing proof-net construction as a middleware paradigm. In: Voronkov, A. (ed.) Automated Deduction\u2014CADE-18. pp. 501\u2013516. Springer Berlin Heidelberg, Berlin, Heidelberg (2002)","DOI":"10.1007\/3-540-45620-1_39"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Andreoli, J.M., Mazar\u00e9, L.: Concurrent construction of proof-nets. In: Baaz, M., Makowsky, J.A. (eds.) Computer Science Logic. pp. 29\u201342. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45220-1_3"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Aschieri, F., Genco, F.A.: Par means parallel: multiplicative linear logic proofs as concurrent functional programs. Proc. ACM Program. Lang. 4(POPL) (dec 2019). https:\/\/doi.org\/10.1145\/3371086, https:\/\/doi.org\/10.1145\/3371086","DOI":"10.1145\/3371086"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Baelde, D., Doumane, A., Saurin, A.: Infinitary proof theory: the multiplicative additive case. In: Talbot, J., Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France. LIPIcs, vol.\u00a062, pp. 42:1\u201342:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.42, https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.42","DOI":"10.4230\/LIPIcs.CSL.2016.42"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04790, pp. 92\u2013106. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_9, https:\/\/doi.org\/10.1007\/978-3-540-75560-9_9","DOI":"10.1007\/978-3-540-75560-9_9"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Bellin, G., Scott, P.: On the $$\\pi $$-calculus and linear logic. Theoretical Computer Science 135(1), 11\u201365 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)00104-9, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397594001049","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Bernardi, G., Hennessy, M.: Mutually Testing Processes. Logical Methods in Computer Science Volume 11, Issue 2 (Apr 2015). https:\/\/doi.org\/10.2168\/LMCS-11(2:1)2015, https:\/\/lmcs.episciences.org\/776","DOI":"10.2168\/LMCS-11(2:1)2015"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Bruscoli, P.: A purely logical account of sequentiality in proof search. In: International Conference on Logic Programming. pp. 302\u2013316. Springer (2002)","DOI":"10.1007\/3-540-45619-8_21"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory. pp. 222\u2013236. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Carbone, M., Cruz-Filipe, L., Montesi, F., Murawska, A.: Multiparty classical choreographies. In: Mesnard, F., Stuckey, P.J. (eds.) Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018, Frankfurt\/Main, Germany, September 4-6, 2018, Revised Selected Papers. Lecture Notes in Computer Science, vol. 11408, pp. 59\u201376. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-13838-7_4, https:\/\/doi.org\/10.1007\/978-3-030-13838-7_4","DOI":"10.1007\/978-3-030-13838-7_4"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Carbone, M., Dardha, O., Montesi, F.: Progress as compositional lock-freedom. In: K\u00fchn, E., Pugliese, R. (eds.) Coordination Models and Languages. pp. 49\u201364. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-662-43376-8_4"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1\u20138:78 (2012). https:\/\/doi.org\/10.1145\/2220365.2220367, https:\/\/doi.org\/10.1145\/2220365.2220367","DOI":"10.1145\/2220365.2220367"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Carbone, M., Lindley, S., Montesi, F., Sch\u00fcrmann, C., Wadler, P.: Coherence generalises duality: A logical explanation of multiparty session types. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Qu\u00e9bec City, Canada. LIPIcs, vol.\u00a059, pp. 33:1\u201333:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2016.33, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.33","DOI":"10.4230\/LIPICS.CONCUR.2016.33"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013. pp. 263\u2013274. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429101, https:\/\/doi.org\/10.1145\/2429069.2429101","DOI":"10.1145\/2429069.2429101"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F., Sch\u00fcrmann, C.: Choreographies, logically. Distributed Comput. 31(1), 51\u201367 (2018). https:\/\/doi.org\/10.1007\/S00446-017-0295-1, https:\/\/doi.org\/10.1007\/s00446-017-0295-1","DOI":"10.1007\/S00446-017-0295-1"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F., Sch\u00fcrmann, C., Yoshida, N.: Multiparty session types as coherence proofs. Acta Informatica 54(3), 243\u2013269 (2017). https:\/\/doi.org\/10.1007\/S00236-016-0285-Y, https:\/\/doi.org\/10.1007\/s00236-016-0285-y","DOI":"10.1007\/S00236-016-0285-Y"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Cockett, J., Seely, R.: Weakly distributive categories. Journal of Pure and Applied Algebra 114(2), 133\u2013173 (1997). https:\/\/doi.org\/10.1016\/0022-4049(95)00160-3, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0022404995001603","DOI":"10.1016\/0022-4049(95)00160-3"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. Math. Struct. Comput. Sci. 26(2), 238\u2013302 (2016). https:\/\/doi.org\/10.1017\/S0960129514000188, https:\/\/doi.org\/10.1017\/S0960129514000188","DOI":"10.1017\/S0960129514000188"},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"Corneil, D., Lerchs, H., Burlingham, L.: Complement reducible graphs. Discrete Applied Mathematics 3(3), 163\u2013174 (1981). https:\/\/doi.org\/10.1016\/0166-218X(81)90013-5, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0166218X81900135","DOI":"10.1016\/0166-218X(81)90013-5"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Larsen, K.S., Montesi, F.: The paths to choreography extraction. In: Esparza, J., Murawski, A.S. (eds.) Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10203, pp. 424\u2013440 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_25, https:\/\/doi.org\/10.1007\/978-3-662-54458-7_25","DOI":"10.1007\/978-3-662-54458-7_25"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F.: Procedural choreographic programming. In: Bouajjani, A., Silva, A. (eds.) Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuch\u00e2tel, Switzerland, June 19-22, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10321, pp. 92\u2013107. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-60225-7_7, https:\/\/doi.org\/10.1007\/978-3-319-60225-7_7","DOI":"10.1007\/978-3-319-60225-7_7"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38\u201366 (2020). https:\/\/doi.org\/10.1016\/J.TCS.2019.07.005, https:\/\/doi.org\/10.1016\/j.tcs.2019.07.005","DOI":"10.1016\/J.TCS.2019.07.005"},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic 28(3), 181\u2013203 (1989). https:\/\/doi.org\/10.1007\/BF01622878, https:\/\/doi.org\/10.1007\/BF01622878","DOI":"10.1007\/BF01622878"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session-typed processes. In: Baier, C., Dal\u00a0Lago, U. (eds.) Foundations of Software Science and Computation Structures. pp. 91\u2013109. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"2_CR36","doi-asserted-by":"publisher","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253\u2013286 (2017). https:\/\/doi.org\/10.1016\/J.IC.2017.06.002, https:\/\/doi.org\/10.1016\/j.ic.2017.06.002","DOI":"10.1016\/J.IC.2017.06.002"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34(1), 83\u2013133 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90113-0, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397584901130","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"De\u00a0Nicola, R., Hennessy, M.: Ccs without $$\\tau $$\u2019s. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT \u201987. pp. 138\u2013152. Springer Berlin Heidelberg, Berlin, Heidelberg (1987)","DOI":"10.1007\/3-540-17660-8_53"},{"key":"2_CR39","doi-asserted-by":"publisher","unstructured":"Fages, F., Ruet, P., Soliman, S.: Linear concurrent constraint programming: Operational and phase semantics. Information and Computation 165(1), 14\u201341 (2001). https:\/\/doi.org\/10.1006\/inco.2000.3002, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540100930025","DOI":"10.1006\/inco.2000.3002"},{"key":"2_CR40","doi-asserted-by":"publisher","unstructured":"Fleury, A., Retor\u00e9, C.: The mix rule. Mathematical Structures in Computer Science 4(2), 273\u2013285 (1994). https:\/\/doi.org\/10.1017\/S0960129500000451","DOI":"10.1017\/S0960129500000451"},{"key":"2_CR41","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 (jul 2002). https:\/\/doi.org\/10.1007\/s001650200016, https:\/\/doi.org\/10.1007\/s001650200016","DOI":"10.1007\/s001650200016"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42, 191\u2013225 (2005)","DOI":"10.1007\/s00236-005-0177-z"},{"key":"2_CR43","doi-asserted-by":"publisher","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science 50(1), 1\u2013101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"2_CR44","unstructured":"Girard, J.Y.: On the meaning of logical rules II: multiplicatives and additives. NATO ASI Series F Computer and Systems Sciences 175, 183\u2013212 (2000)"},{"key":"2_CR45","unstructured":"Guglielmi, A.: Concurrency and plan generation in a logic programming language with a sequential operator. In: ICLP. pp. 240\u2013254. Citeseer (1994)"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"Guglielmi, A.: Sequentiality by linear implication and universal quantification. In: Desel, J. (ed.) Structures in Concurrency Theory. pp. 160\u2013174. Springer London, London (1995)","DOI":"10.1007\/978-1-4471-3078-9_11"},{"key":"2_CR47","doi-asserted-by":"publisher","unstructured":"Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Logic 8(1), 1\u2013es (Jan 2007). https:\/\/doi.org\/10.1145\/1182613.1182614, https:\/\/doi.org\/10.1145\/1182613.1182614","DOI":"10.1145\/1182613.1182614"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic, pp. 99\u2013217. Springer Netherlands, Dordrecht (2002). https:\/\/doi.org\/10.1007\/978-94-017-0456-4_2, https:\/\/doi.org\/10.1007\/978-94-017-0456-4_2","DOI":"10.1007\/978-94-017-0456-4_2"},{"key":"2_CR49","unstructured":"Hennessy, M.: Algebraic theory of processes. MIT Press, Cambridge, MA, USA (1988)"},{"key":"2_CR50","doi-asserted-by":"crossref","unstructured":"Hennessy, M.: A distributed Pi-calculus. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511611063"},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de\u00a0Bakker, J., van Leeuwen, J. (eds.) Automata, Languages and Programming. pp. 299\u2013309. Springer Berlin Heidelberg, Berlin, Heidelberg (1980)","DOI":"10.1007\/3-540-10003-2_79"},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (oct 1969). https:\/\/doi.org\/10.1145\/363235.363259, https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"2_CR53","doi-asserted-by":"publisher","unstructured":"Hodas, J., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Information and Computation 110(2), 327\u2013365 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1036, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540184710364","DOI":"10.1006\/inco.1994.1036"},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"Holmstr\u00f6m, S.: Hennessy-milner logic with recursion as a specification language, and a refinement calculus based on it. In: Rattray, C. (ed.) Specification and Verification of Concurrent Systems. pp. 294\u2013330. Springer London, London (1990)","DOI":"10.1007\/978-1-4471-3534-0_15"},{"key":"2_CR55","doi-asserted-by":"crossref","unstructured":"Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR\u201993. pp. 509\u2013523. Springer Berlin Heidelberg, Berlin, Heidelberg (1993)","DOI":"10.1007\/3-540-57208-2_35"},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) Programming Languages and Systems. pp. 122\u2013138. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)","DOI":"10.1007\/BFb0053567"},{"key":"2_CR57","doi-asserted-by":"publisher","unstructured":"Horne, R., Tiu, A.: Constructing weak simulations from linear implications for processes with private names. Mathematical Structures in Computer Science 29(8), 1275\u20131308 (2019). https:\/\/doi.org\/10.1017\/S09601295","DOI":"10.1017\/S09601295"},{"key":"2_CR58","doi-asserted-by":"publisher","unstructured":"Horne, R., Tiu, A., Aman, B., Ciobanu, G.: Private Names in Non-Commutative Logic. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a059, pp. 31:1\u201331:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.31, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CONCUR.2016.31","DOI":"10.4230\/LIPIcs.CONCUR.2016.31"},{"key":"2_CR59","doi-asserted-by":"publisher","unstructured":"Horne, R., Tiu, A., Aman, B., Ciobanu, G.: De morgan dual nominal quantifiers modelling private names in non-commutative logic. ACM Trans. Comput. Logic 20(4) (jul 2019). https:\/\/doi.org\/10.1145\/3325821, https:\/\/doi.org\/10.1145\/3325821","DOI":"10.1145\/3325821"},{"key":"2_CR60","doi-asserted-by":"publisher","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. The Journal of Logic Programming 19-20, 503\u2013581 (1994). https:\/\/doi.org\/10.1016\/0743-1066(94)90033-7, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0743106694900337, special Issue: Ten Years of Logic Programming","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Kj\u00e6r, B.A., Cruz-Filipe, L., Montesi, F.: From infinity to choreographies: Extraction for unbounded systems (2022)","DOI":"10.1007\/978-3-031-16767-6_6"},{"key":"2_CR62","doi-asserted-by":"publisher","unstructured":"Kobayashi, N.: A type system for lock-free processes. Information and Computation 177(2), 122\u2013159 (2002). https:\/\/doi.org\/10.1006\/inco.2002.3171, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540102931718","DOI":"10.1006\/inco.2002.3171"},{"key":"2_CR63","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914\u2013947 (1999). https:\/\/doi.org\/10.1145\/330249.330251, https:\/\/doi.org\/10.1145\/330249.330251","DOI":"10.1145\/330249.330251"},{"key":"2_CR64","doi-asserted-by":"publisher","unstructured":"Kokke, W., Montesi, F., Peressotti, M.: Better late than never: a fully-abstract semantics for classical processes. Proc. ACM Program. Lang. 3(POPL) (jan 2019). https:\/\/doi.org\/10.1145\/3290337, https:\/\/doi.org\/10.1145\/3290337","DOI":"10.1145\/3290337"},{"key":"2_CR65","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theoretical Computer Science 27(3), 333\u2013354 (1983). https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397582901256, special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"2_CR66","doi-asserted-by":"publisher","unstructured":"Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. SIGPLAN Not. 50(1), 221\u2013232 (jan 2015). https:\/\/doi.org\/10.1145\/2775051.2676964, https:\/\/doi.org\/10.1145\/2775051.2676964","DOI":"10.1145\/2775051.2676964"},{"key":"2_CR67","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Studies in Logic and the Foundations of Mathematics, vol.\u00a0104, pp. 153\u2013175. Elsevier (1982)","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"2_CR68","doi-asserted-by":"crossref","unstructured":"Menni, M.: About &-quantifiers. Applied categorical structures 11, 421\u2013445 (2003)","DOI":"10.1023\/A:1025750816098"},{"key":"2_CR69","unstructured":"Miller, D.: Hereditary harrop formulas and logic programming. In: Proceedings of the VIII International Congress of Logic, Methodology, and Philosophy of Science. pp. 153\u2013156 (1987)"},{"key":"2_CR70","doi-asserted-by":"crossref","unstructured":"Miller, D.: Abstract syntax and logic programming. In: Voronkov, A. (ed.) Logic Programming. pp. 322\u2013337. Springer Berlin Heidelberg, Berlin, Heidelberg (1992)","DOI":"10.1007\/3-540-55460-2_24"},{"key":"2_CR71","doi-asserted-by":"crossref","unstructured":"Miller, D.: The $$\\pi $$-calculus as a theory in linear logic: Preliminary results. In: Lamma, E., Mello, P. (eds.) Extensions of Logic Programming. pp. 242\u2013264. Springer Berlin Heidelberg, Berlin, Heidelberg (1993)","DOI":"10.1007\/3-540-56454-3_13"},{"key":"2_CR72","doi-asserted-by":"publisher","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51(1), 125\u2013157 (1991). https:\/\/doi.org\/10.1016\/0168-0072(91)90068-W, https:\/\/www.sciencedirect.com\/science\/article\/pii\/016800729190068W","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"2_CR73","doi-asserted-by":"publisher","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Logic 6(4), 749\u2013783 (oct 2005). https:\/\/doi.org\/10.1145\/1094622.1094628, https:\/\/doi.org\/10.1145\/1094622.1094628","DOI":"10.1145\/1094622.1094628"},{"key":"2_CR74","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.\u00a092. Springer (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3, https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"2_CR75","doi-asserted-by":"publisher","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, i. Information and Computation 100(1), 1\u201340 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90008-4, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0890540192900084","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"2_CR76","doi-asserted-by":"publisher","unstructured":"Montanari, U.: Networks of constraints: Fundamental properties and applications to picture processing. Information Sciences 7, 95\u2013132 (1974). https:\/\/doi.org\/10.1016\/0020-0255(74)90008-5, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0020025574900085","DOI":"10.1016\/0020-0255(74)90008-5"},{"key":"2_CR77","unstructured":"Montesi, F.: Choreographic Programming. Ph.D. thesis, IT University of Copenhagen (2013), https:\/\/www.fabriziomontesi.com\/files\/choreographic-programming.pdf"},{"key":"2_CR78","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":"2_CR79","doi-asserted-by":"publisher","unstructured":"Montesi, F., Yoshida, N.: Compositional choreographies. In: D\u2019Argenio, P.R., Melgratti, H.C. (eds.) CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08052, pp. 425\u2013439. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_30, https:\/\/doi.org\/10.1007\/978-3-642-40184-8_30","DOI":"10.1007\/978-3-642-40184-8_30"},{"key":"2_CR80","doi-asserted-by":"publisher","unstructured":"Olarte, C., Pimentel, E.: On concurrent behaviors and focusing in linear logic. Theoretical Computer Science 685, 46\u201364 (2017). https:\/\/doi.org\/10.1016\/j.tcs.2016.08.026, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397516304832, logical and Semantic Frameworks with Applications","DOI":"10.1016\/j.tcs.2016.08.026"},{"key":"2_CR81","doi-asserted-by":"publisher","unstructured":"Olarte, C., Pimentel, E., Nigam, V.: Subexponential concurrent constraint programming. Theoretical Computer Science 606, 98\u2013120 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.06.031, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397515005411, logical and Semantic Frameworks with Applications","DOI":"10.1016\/j.tcs.2015.06.031"},{"key":"2_CR82","doi-asserted-by":"crossref","unstructured":"Olarte, C., Rueda, C., Valencia, F.D.: Models and emerging trends of concurrent constraint programming. Constraints 18, 535\u2013578 (2013)","DOI":"10.1007\/s10601-013-9145-3"},{"key":"2_CR83","doi-asserted-by":"publisher","unstructured":"Padovani, L.: Deadlock and lock freedom in the linear $$\\pi $$-calculus. 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). CSL-LICS \u201914, Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2603088.2603116, https:\/\/doi.org\/10.1145\/2603088.2603116","DOI":"10.1145\/2603088.2603116"},{"key":"2_CR84","doi-asserted-by":"publisher","unstructured":"Pimentel, E., Olarte, C., Nigam, V.: Process-As-Formula Interpretation: A Substructural Multimodal View. In: Kobayashi, N. (ed.) 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0195, pp. 3:1\u20133:21. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.3, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2021.3","DOI":"10.4230\/LIPIcs.FSCD.2021.3"},{"key":"2_CR85","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 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":"2_CR86","doi-asserted-by":"publisher","unstructured":"Roversi, L.: A deep inference system with a self-dual binder which is complete for linear lambda calculus. Journal of Logic and Computation 26(2), 677\u2013698 (2016). https:\/\/doi.org\/10.1093\/logcom\/exu033","DOI":"10.1093\/logcom\/exu033"},{"key":"2_CR87","doi-asserted-by":"publisher","unstructured":"Sangiorgi, D.: Pi-i: A symmetric calculus based on internal mobility. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds.) TAPSOFT\u201995: Theory and Practice of Software Development, 6th International Joint Conference CAAP\/FASE, Aarhus, Denmark, May 22-26, 1995, Proceedings. Lecture Notes in Computer Science, vol.\u00a0915, pp. 172\u2013186. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-59293-8_194, https:\/\/doi.org\/10.1007\/3-540-59293-8_194","DOI":"10.1007\/3-540-59293-8_194"},{"key":"2_CR88","doi-asserted-by":"publisher","unstructured":"Saraswat, V.A., Rinard, M.: Concurrent constraint programming. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 232\u2013245. POPL \u201990, Association for Computing Machinery, New York, NY, USA (1989). https:\/\/doi.org\/10.1145\/96709.96733, https:\/\/doi.org\/10.1145\/96709.96733","DOI":"10.1145\/96709.96733"},{"key":"2_CR89","doi-asserted-by":"publisher","unstructured":"Shapiro, E.: The family of concurrent logic programming languages. ACM Comput. Surv. 21(3), 413\u2013510 (sep 1989). https:\/\/doi.org\/10.1145\/72551.72555, https:\/\/doi.org\/10.1145\/72551.72555","DOI":"10.1145\/72551.72555"},{"key":"2_CR90","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard isomorphism. Elsevier (2006)","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"2_CR91","doi-asserted-by":"publisher","unstructured":"Tiu, A.: A System of Interaction and Structure II: The Need for Deep Inference. Logical Methods in Computer Science Volume 2, Issue 2 (Apr 2006). https:\/\/doi.org\/10.2168\/LMCS-2(2:4)2006, https:\/\/lmcs.episciences.org\/2252","DOI":"10.2168\/LMCS-2(2:4)2006"},{"key":"2_CR92","doi-asserted-by":"crossref","unstructured":"Torres\u00a0Vieira, H., Thudichum\u00a0Vasconcelos, V.: Typing progress in communication-centred systems. In: De\u00a0Nicola, R., Julien, C. (eds.) Coordination Models and Languages. pp. 236\u2013250. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38493-6_17"},{"key":"2_CR93","doi-asserted-by":"publisher","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2 edn. (2000). https:\/\/doi.org\/10.1017\/CBO9781139168717","DOI":"10.1017\/CBO9781139168717"},{"key":"2_CR94","doi-asserted-by":"crossref","unstructured":"Valdes, J., Tarjan, R.E., Lawler, E.L.: The recognition of series parallel digraphs. In: Proceedings of the eleventh annual ACM symposium on Theory of computing. pp. 1\u201312. ACM (1979)","DOI":"10.1145\/800135.804393"},{"key":"2_CR95","doi-asserted-by":"publisher","unstructured":"Vasconcelos, V.T.: Fundamentals of session types. Information and Computation 217, 52\u201370 (2012). https:\/\/doi.org\/10.1016\/j.ic.2012.05.002, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540112001022","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"2_CR96","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Propositions as sessions. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. p. 273\u2013286. ICFP \u201912, Association for Computing Machinery, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2364527.2364568, https:\/\/doi.org\/10.1145\/2364527.2364568","DOI":"10.1145\/2364527.2364568"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91118-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:32Z","timestamp":1746001052000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91118-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911170","9783031911187"],"references-count":96,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91118-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}