{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:40Z","timestamp":1775873680882,"version":"3.50.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K034413\/1, EP\/K011715\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1"],"award-info":[{"award-number":["EP\/K034413\/1, EP\/K011715\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000921","name":"European Cooperation in Science and Technology","doi-asserted-by":"publisher","award":["CA15123"],"award-info":[{"award-number":["CA15123"]}],"id":[{"id":"10.13039\/501100000921","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n            Multiparty Session Types (MPST) are a typing discipline ensuring that a message-passing process implements a\n            <jats:italic>multiparty session protocol<\/jats:italic>\n            , without errors. In this paper, we propose a new, generalised MPST theory.\n          <\/jats:p>\n          <jats:p>\n            Our contribution is fourfold. (1) We demonstrate that a revision of the theoretical foundations of MPST is\n            <jats:italic>necessary<\/jats:italic>\n            : classic MPST have a limited\n            <jats:italic>subject reduction<\/jats:italic>\n            property, with inherent restrictions that are easily overlooked, and in previous work have led to flawed type safety proofs; our new theory removes such restrictions and fixes such flaws. (2) We contribute a new MPST theory that is\n            <jats:italic>less<\/jats:italic>\n            complicated, and yet\n            <jats:italic>more<\/jats:italic>\n            general, than the classic one: it does\n            <jats:italic>not<\/jats:italic>\n            require\n            <jats:italic>global multiparty session types<\/jats:italic>\n            nor\n            <jats:italic>binary session type duality<\/jats:italic>\n            \u2014 instead, it is grounded on general behavioural type-level properties, and proves type safety of many more protocols and processes. (3) We produce a detailed analysis of type-level properties, showing how, in our new theory, they allow to ensure decidability of type checking, and statically guarantee that processes enjoy, , deadlock-freedom and liveness at run-time. (4) We show how our new theory can integrate type and model checking: type-level properties can be expressed in modal \u00b5-calculus, and verified with well-established tools.\n          <\/jats:p>","DOI":"10.1145\/3290343","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":80,"title":["Less is more: multiparty session types revisited"],"prefix":"10.1145","volume":"3","author":[{"given":"Alceste","family":"Scalas","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"e_1_2_2_2_1","volume-title":"Honesty by Typing. LMCS 12(4)","author":"Bartoletti Massimo","year":"2016"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1963405.1963516"},{"key":"e_1_2_2_4_1","volume-title":"On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci. 656","author":"Basu Samik","year":"2016"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_5"},{"key":"e_1_2_2_6_1","volume-title":"Using higher-order contracts to model session types. LMCS 12(2)","author":"Bernardi Giovanni","year":"2016"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"e_1_2_2_8_1","volume-title":"Meeting Deadlines Together. In CONCUR.","author":"Bocchi Laura","year":"2015"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950999017X"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39570-8_6"},{"key":"e_1_2_2_12_1","volume-title":"Linear logic propositions as session types. MSCS 26, 3","author":"Caires Lu\u00eds","year":"2016"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","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 CONCUR.  Marco Carbone Sam Lindley Fabrizio Montesi Carsten Sch\u00fcrmann and Philip Wadler. 2016. Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. In CONCUR.","DOI":"10.1007\/s00236-016-0285-y"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Marco Carbone Fabrizio Montesi Carsten Sch\u00fcrmann and Nobuko Yoshida. 2015. Multiparty Session Types as Coherence Proofs. In CONCUR.  Marco Carbone Fabrizio Montesi Carsten Sch\u00fcrmann and Nobuko Yoshida. 2015. Multiparty Session Types as Coherence Proofs. In CONCUR.","DOI":"10.1007\/s00236-016-0285-y"},{"key":"e_1_2_2_15_1","volume-title":"On the Preciseness of Subtyping in Session Types. Logical Methods in Computer Science 13, 2","author":"Chen Tzu-Chun","year":"2017"},{"key":"e_1_2_2_16_1","volume-title":"Lightening global types. JLAMP 84, 5","author":"Chen Tzu-Chun","year":"2015"},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"Mario Coppo Mariangiola Dezani-Ciancaglini Luca Padovani and Nobuko Yoshida. 2015a. A Gentle Introduction to Multiparty Asynchronous Session Types. In Formal Methods for Multicore Programming.  Mario Coppo Mariangiola Dezani-Ciancaglini Luca Padovani and Nobuko Yoshida. 2015a. A Gentle Introduction to Multiparty Asynchronous Session Types. In Formal Methods for Multicore Programming.","DOI":"10.1007\/978-3-319-18941-3_4"},{"key":"e_1_2_2_18_1","volume-title":"Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS 760","author":"Coppo Mario","year":"2015"},{"key":"e_1_2_2_19_1","volume-title":"Parameterised Multiparty Session Types. LMCS 8, 4","author":"Deni\u00e9lou Pierre-Malo","year":"2012"},{"key":"e_1_2_2_20_1","volume-title":"Multiparty Session Types Meet Communicating Automata. In ESOP.","author":"Deni\u00e9lou Pierre-Malo","year":"2012"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Pierre-Malo Deni\u00e9lou and Nobuko Yoshida. 2013. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In ICALP.  Pierre-Malo Deni\u00e9lou and Nobuko Yoshida. 2013. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In ICALP.","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Mariangiola Dezani-Ciancaglini Silvia Ghilezan Svetlana Jaksic Jovanka Pantovic and Nobuko Yoshida. 2015. Precise subtyping for synchronous multiparty sessions. In PLACES.  Mariangiola Dezani-Ciancaglini Silvia Ghilezan Svetlana Jaksic Jovanka Pantovic and Nobuko Yoshida. 2015. Precise subtyping for synchronous multiparty sessions. In PLACES.","DOI":"10.4204\/EPTCS.203.3"},{"key":"e_1_2_2_23_1","unstructured":"Alain Finkel and Etienne Lozes. 2017. Synchronizability of Communicating Finite State Machines is not Decidable. In ICALP.  Alain Finkel and Etienne Lozes. 2017. Synchronizability of Communicating Finite State Machines is not Decidable. In ICALP."},{"key":"e_1_2_2_24_1","volume-title":"Behavioural Types: From Theory to Tools","author":"Gay Simon","year":"2017"},{"key":"e_1_2_2_25_1","volume-title":"A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (LNCS)","author":"Gay Simon J."},{"key":"e_1_2_2_26_1","unstructured":"Simon J. Gay Nils Gesbert and Ant\u00f3nio Ravara. 2014. Session Types as Generic Process Types. In EXPRESS\/SOS.  Simon J. Gay Nils Gesbert and Ant\u00f3nio Ravara. 2014. Session Types as Generic Process Types. In EXPRESS\/SOS."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"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","volume-title":"An extensible approach to session polymorphism. Mathematical Structures in Computer Science 26, 3","author":"Goto Matthew","year":"2016"},{"key":"e_1_2_2_30_1","volume-title":"Modeling and Analysis of Communicating Systems","author":"Groote Jan Friso"},{"key":"e_1_2_2_31_1","unstructured":"Chaodong He. 2011. The Decidability of the Reachability Problem for CCS!. In CONCUR.   Chaodong He. 2011. The Decidability of the Reachability Problem for CCS!. In CONCUR."},{"key":"e_1_2_2_32_1","volume-title":"Vasco Thudichum Vasconcelos, and Makoto Kubo","author":"Honda Kohei","year":"1998"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873052"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00325-6"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1745312.1745313"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676964"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_2_41_1","unstructured":"OAuth Working Group. 2012. RFC 6749: OAuth 2.0 Framework. http:\/\/tools.ietf.org\/html\/rfc6749 .  OAuth Working Group. 2012. RFC 6749: OAuth 2.0 Framework. http:\/\/tools.ietf.org\/html\/rfc6749 ."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_2_2_43_1","volume-title":"Fair Subtyping for Multi-Party Session Types. Mathematical Structures in Computer Science 26, 3","author":"Padovani Luca","year":"2016"},{"key":"e_1_2_2_44_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C."},{"key":"e_1_2_2_45_1","unstructured":"Alceste Scalas Ornela Dardha Raymond Hu and Nobuko Yoshida. 2017a. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In ECOOP.  Alceste Scalas Ornela Dardha Raymond Hu and Nobuko Yoshida. 2017a. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In ECOOP."},{"key":"e_1_2_2_46_1","volume-title":"A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact). Dagstuhl Artifacts Series 3, 1","author":"Scalas Alceste","year":"2017"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.01.001"},{"key":"e_1_2_2_49_1","volume-title":"A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (LNCS)","author":"Toninho Bernardo"},{"key":"e_1_2_2_50_1","volume-title":"Certifying data in multiparty session types. JLAMP 90","author":"Toninho Bernardo","year":"2017"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_10"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290343","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290343","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290343"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":51,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290343"],"URL":"https:\/\/doi.org\/10.1145\/3290343","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}