{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:08:10Z","timestamp":1762459690278,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,12,13]],"date-time":"2018-12-13T00:00:00Z","timestamp":1544659200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100005856","name":"Faculdade de Ci\u00eancias e Tecnologia, Universidade Nova de Lisboa","doi-asserted-by":"publisher","award":["UID\/CEC\/04516\/2013"],"award-info":[{"award-number":["UID\/CEC\/04516\/2013"]}],"id":[{"id":"10.13039\/501100005856","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K0.4413\/1,EP\/K011715\/1,EP\/L00058X\/1,EP\/N027833\/1,EP\/N028201\/1"],"award-info":[{"award-number":["EP\/K0.4413\/1,EP\/K011715\/1,EP\/L00058X\/1,EP\/N027833\/1,EP\/N028201\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2018,12,31]]},"abstract":"<jats:p>In multiparty session types, interconnection networks identify which roles in a session engage in communication (i.e., two roles are connected if they exchange a message). In session-based interpretations of linear logic the analogue notion corresponds to determining which processes are composed, or cut, using compatible channels typed by linear propositions. In this work, we show that well-formed interactions represented in a session-based interpretation of classical linear logic (CLL) form strictly less-expressive interconnection networks than those of a multiparty session calculus. To achieve this result, we introduce a new compositional synthesis property dubbed partial multiparty compatibility (PMC), enabling us to build a global type denoting the interactions obtained by iterated composition of well-typed CLL threads. We then show that CLL composition induces PMC global types without circular interconnections between three (or more) participants. PMC is then used to define a new CLL composition rule that can form circular interconnections but preserves the deadlock-freedom of CLL.<\/jats:p>","DOI":"10.1145\/3242173","type":"journal-article","created":{"date-parts":[[2018,12,13]],"date-time":"2018-12-13T15:45:03Z","timestamp":1544715903000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Interconnectability of Session-Based Logical Processes"],"prefix":"10.1145","volume":"40","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0746-7514","authenticated-orcid":false,"given":"Bernardo","family":"Toninho","sequence":"first","affiliation":[{"name":"NOVA-LINCS, Universidade Nova de Lisboa and Imperial College London, Caparica, Portugal"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2018,12,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","unstructured":"Samson Abramsky Simon J. Gay and Rajagopal Nagarajan. 1995. Specification structures and propositions-as-types for concurrency. In Logics for Concurrency. 5--40.","DOI":"10.5555\/239519.239520"},{"volume-title":"A List of Successes That Can Change the World\u2014Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, LNCS","author":"Atkey Robert","key":"e_1_2_2_3_1","unstructured":"Robert Atkey, Sam Lindley, and J. Garrett Morris. 2016. Conflation confers concurrency. In A List of Successes That Can Change the World\u2014Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, LNCS, Vol. 9600. Springer, 32--55."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.02.009"},{"key":"e_1_2_2_6_1","volume-title":"Meeting deadlines together. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201915)","volume":"42","author":"Bocchi Laura","year":"2015","unstructured":"Laura Bocchi, Julien Lange, and Nobuko Yoshida. 2015. Meeting deadlines together. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201915), Vol. 42. Schloss Dagstuhl, 283--296."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39570-8_6"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887670"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000619"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201916), Leibniz International Proceedings in Informatics","volume":"59","author":"Carbone Marco","year":"2016","unstructured":"Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Sch\u00fcrmann, and Philip Wadler. 2016. Coherence generalises duality: A logical explanation of multiparty session types. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201916), Leibniz International Proceedings in Informatics, Vol. 59. Schloss Dagstuhl, 33:1--33:15."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429101"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_5"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201915), Leibniz International Proceedings in Informatics","volume":"42","author":"Carbone Marco","year":"2015","unstructured":"Marco Carbone, Fabrizio Montesi, Carsten Sch\u00fcrmann, and Nobuko Yoshida. 2015. Multiparty session types as coherence proofs. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201915), Leibniz International Proceedings in Informatics, Vol. 42. Schloss Dagstuhl, 412--426."},{"key":"e_1_2_2_15_1","volume-title":"Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201917)","volume":"85","author":"Castellani Ilaria","year":"2017","unstructured":"Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. 2017. Concurrent reversible sessions. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201917), LIPIcs, Vol. 85. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, 30:1--30:17."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0381-3"},{"key":"e_1_2_2_17_1","volume-title":"On the preciseness of subtyping in session types. Logic. Methods Comput. Sci. 13, 2","author":"Chen Tzu-Chun","year":"2017","unstructured":"Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. 2017. On the preciseness of subtyping in session types. Logic. Methods Comput. Sci. 13, 2 (2017)."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000188"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.190.1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0218-8"},{"key":"e_1_2_2_21_1","volume-title":"Leibniz International Proceedings in Informatics (LIPIcs)","volume":"45","author":"Demangeon Romain","year":"2015","unstructured":"Romain Demangeon and Nobuko Yoshida. 2015. On the expressiveness of multiparty sessions. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201915), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 45. Schloss Dagstuhl, 560--574."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"e_1_2_2_23_1","unstructured":"Henry DeYoung Luis Caires Frank Pfenning and Bernardo Toninho. 2012. Cut reduction in linear logic as asynchronous session-typed communication. In Computer Science Logic."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45917-1_8"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.223.3"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"volume-title":"A List of Successes That Can Change the World\u2014Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 95--108.","author":"Gay Simon J.","key":"e_1_2_2_27_1","unstructured":"Simon J. Gay. 2016. Subtyping supports safe session substitution. In A List of Successes That Can Change the World\u2014Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 95--108."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645392.651876"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_24"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54494-5_7"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873052"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837662"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_17"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676964"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_52"},{"key":"e_1_2_2_39_1","volume-title":"Conference name is European Symposium on Programming (ESOP'15)","volume":"9032","author":"Lindley Sam","unstructured":"Sam Lindley and J. Garrett Morris. 2015. A semantics for propositions as sessions. In Conference name is European Symposium on Programming (ESOP'15) (LNCS), Vol. 9032. Springer, 560--584."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814302"},{"key":"e_1_2_2_42_1","unstructured":"Mungo 2016. Mungo homepage. Retrieved from http:\/\/www.dcs.gla.ac.uk\/research\/mungo\/."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0420-8"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","unstructured":"Rumyana Neykova Raymond Hu Nobuko Yoshida and Fahd Abdeljallal. 2018. Session type provider: Compile-time API generation for distributed protocols in F#. (unpublished). 10.1145\/3178372.3179495","DOI":"10.1145\/3178372.3179495"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3033019.3033031"},{"key":"e_1_2_2_46_1","volume-title":"Multiparty session actors. Logical Methods Comput. Sci. 13, 1","author":"Neykova Rumyana","year":"2017","unstructured":"Rumyana Neykova and Nobuko Yoshida. 2017. Multiparty session actors. Logical Methods Comput. Sci. 13, 1 (2017)."},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_11"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892232"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30561-0_15"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43376-8_10"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_27"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_18"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"e_1_2_2_54_1","volume-title":"Proceedings of the 31st European Conference on Object-Oriented Programming (ECOOP\u201917), Leibniz International Proceedings in Informatics","volume":"74","author":"Scalas Alceste","year":"2017","unstructured":"Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. 2017. A linear decomposition of multiparty sessions for safe distributed programming. In Proceedings of the 31st European Conference on Object-Oriented Programming (ECOOP\u201917), Leibniz International Proceedings in Informatics, Vol. 74. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, 24:1--24:31."},{"key":"e_1_2_2_55_1","unstructured":"Scribble. 2008. Scribble Project. Retrieved from www.scribble.org."},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.03.004"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDP.2016.72"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_2_2_59_1","volume-title":"International Conference on Coordination Models and Language (COORDINATION) 2013 (LNCS)","volume":"7890","author":"Vieira Hugo Torres","year":"2013","unstructured":"Hugo Torres Vieira and Vasco Thudichum Vasconcelos. 2013. Typing progress in communication-centred systems. In International Conference on Coordination Models and Language (COORDINATION) 2013 (LNCS), Vol. 7890. Springer, 236--250."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3242173","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3242173","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:36Z","timestamp":1750207416000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3242173"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,13]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,12,31]]}},"alternative-id":["10.1145\/3242173"],"URL":"https:\/\/doi.org\/10.1145\/3242173","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2018,12,13]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}