{"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":1775873680268,"version":"3.50.1"},"reference-count":43,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,15]],"date-time":"2012-03-15T00:00:00Z","timestamp":1331769600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Global types are formal specifications that describe communication protocols in terms of their global interactions. We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions obtained projecting our global types enjoy a liveness property in addition to the traditional progress and are shown to be sound and complete with respect to the set of traces of the originating global type. Our notion of completeness is less demanding than the classical ones, allowing a multi-party session to leave out redundant traces from an underspecified global type. In addition to the technical content, we discuss some limitations of our language of global types and provide an extensive comparison with related specification languages adopted in different communities.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:24)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":60,"title":["On Global Types and Multi-Party Session"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Giuseppe","family":"Castagna","sequence":"first","affiliation":[]},{"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9097-1297","authenticated-orcid":false,"given":"Luca","family":"Padovani","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,15]]},"reference":[{"key":"10.2168\/LMCS-8(1:24)2012_Alur00","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis. Inference of message sequence charts. InProceedings of ICSE'00, pages 304-313. ACM Press, 2000.","DOI":"10.1145\/337180.337215"},{"key":"10.2168\/LMCS-8(1:24)2012_Alur01","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis. Realizability and verification of MSC graphs. InProceedings of ICALP'01, LNCS 2076, pages 797-808. Springer, 2001.","DOI":"10.1007\/3-540-48224-5_65"},{"key":"10.2168\/LMCS-8(1:24)2012_spi99","first-page":"36","volume":"148","author":"Mart\u00edn Abadi and Andrew D. Gordon","year":"1999","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(1:24)2012_AY99","doi-asserted-by":"crossref","unstructured":"Rajeev Alur and Mihalis Yannakakis. Model checking of message sequence charts. InProceedings of CONCUR'99, LNCS 1664, pages 114-129. Springer, 1999.","DOI":"10.1007\/3-540-48320-9_10"},{"key":"10.2168\/LMCS-8(1:24)2012_BasuBultan11","doi-asserted-by":"crossref","unstructured":"Samik Basu and Tevfik Bultan. Choreography conformance via synchronizability. InProceedings of WWW'11, pages 795-804. ACM Press, 2011.","DOI":"10.1145\/1963405.1963516"},{"key":"10.2168\/LMCS-8(1:24)2012_BBCDPS09","unstructured":"Matteo Baldoni, Cristina Baroglio, Amit K. Chopra, Nirmit Desai, Viviana Patti, and Munindar P. Singh. Choice, interoperability, and conformance in interaction protocols and service choreographies. InProceedings of AAMAS'09, pages 843-850. International Foundation for Autonomous Agents and Multiagent Systems, 2009."},{"key":"10.2168\/LMCS-8(1:24)2012_BBDL08","doi-asserted-by":"crossref","unstructured":"Michele Boreale, Roberto Bruni, Rocco De Nicola, and Michele Loreti. Sessions and pipelines for structured service programming. InProceedings of FMOODS'08, LNCS 5051, pages 19-38. Springer, 2008.","DOI":"10.1007\/978-3-540-68863-1_3"},{"key":"10.2168\/LMCS-8(1:24)2012_BergstraBethkePonse93","unstructured":"Jan A. Bergstra, Inge Bethke, and Alban Ponse. Process algebra with iteration. Technical Report Report CS-R9314, Programming Research Group, University of Amsterdam, 1993."},{"key":"10.2168\/LMCS-8(1:24)2012_BCDDDY08","doi-asserted-by":"crossref","unstructured":"Lorenzo Bettini, Mario Coppo, Loris D'Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. Global progress in dynamically interleaved multiparty sessions. InProceedings of CONCUR'08, LNCS 5201, pages 418-433. Springer, 2008.","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"10.2168\/LMCS-8(1:24)2012_BCDFL09","doi-asserted-by":"crossref","unstructured":"Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deni\u00e9lou, C\u00e9dric Fournet, and James J. Leifer. Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. InProceedings of CSF'09, pages 124-140. IEEE Computer Society, 2009.","DOI":"10.1109\/CSF.2009.26"},{"key":"10.2168\/LMCS-8(1:24)2012_BLZ08","doi-asserted-by":"crossref","unstructured":"Mario Bravetti, Ivan Lanese, and Gianluigi Zavattaro. Contract-driven implementation of choreographies. InProceedings of TGC'08, LNCS 5474, pages 1-18. Springer, 2008.","DOI":"10.1007\/978-3-642-00945-7_1"},{"key":"10.2168\/LMCS-8(1:24)2012_BZ93","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"10.2168\/LMCS-8(1:24)2012_BZ07","doi-asserted-by":"crossref","unstructured":"Mario Bravetti and Gianluigi Zavattaro. Towards a unifying theory for choreography conformance and contract compliance. InProceedings of SC'07, LNCS 4829, pages 34-50. Springer, 2007.","DOI":"10.1007\/978-3-540-77351-1_4"},{"key":"10.2168\/LMCS-8(1:24)2012_BZ08","doi-asserted-by":"crossref","unstructured":"Mario Bravetti and Gianluigi Zavattaro. Contract compliance and choreography conformance in the presence of message queues. InProceedings of WS-FM'08, LNCS 5387, pages 37-54. Springer, 2008.","DOI":"10.1007\/978-3-642-01364-5_3"},{"key":"10.2168\/LMCS-8(1:24)2012_Car94","doi-asserted-by":"crossref","unstructured":"Ulf Carlsen. Generating formal cryptographic protocol specifications. InProceedings of the IEEE Symposium on Security and Privacy, pages 137-146. IEEE Computer Society, 1994.","DOI":"10.1109\/RISP.1994.296586"},{"key":"10.2168\/LMCS-8(1:24)2012_CeceFinkel05","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.05.006"},{"key":"10.2168\/LMCS-8(1:24)2012_carbone.honda.yoshida:esop07","doi-asserted-by":"crossref","unstructured":"Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centred programming for web services. InProceedings of ESOP'07, LNCS 4421, pages 2-17. Springer, 2007.","DOI":"10.1007\/978-3-540-71316-6_2"},{"key":"10.2168\/LMCS-8(1:24)2012_CP09","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna and Luca Padovani. Contracts for mobile processes. InProceedings of CONCUR'09, LNCS 5710, pages 211-228. Springer, 2009.","DOI":"10.1007\/978-3-642-04081-8_15"},{"key":"10.2168\/LMCS-8(1:24)2012_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2009.11.004"},{"key":"10.2168\/LMCS-8(1:24)2012_CV09","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Caires and Hugo Torres Vieira. Conversation types. InProceedings of ESOP'09, LNCS 5502, pages 285-300. Springer, 2009.","DOI":"10.1007\/978-3-642-00590-9_21"},{"key":"10.2168\/LMCS-8(1:24)2012_Cal06","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.041"},{"key":"10.2168\/LMCS-8(1:24)2012_CZ08","doi-asserted-by":"crossref","unstructured":"Cai Chao and Qiu Zongyan. An approach to check choreography with channel passing in WS-CDL. InProceedings of ICWS'08, pages 700-707. IEEE Computer Society, 2008.","DOI":"10.1109\/ICWS.2008.46"},{"key":"10.2168\/LMCS-8(1:24)2012_DLY07","doi-asserted-by":"crossref","unstructured":"Mariangiola Dezani-Ciancaglini, Ugo de' Liguoro, and Nobuko Yoshida. On progress for structured communications. InProceedings of TGC'07, LNCS 4912, pages 257-275. Springer, 2008.","DOI":"10.1007\/978-3-540-78663-4_18"},{"key":"10.2168\/LMCS-8(1:24)2012_DY11","doi-asserted-by":"crossref","unstructured":"Pierre-Malo Deni\u00e9lou and Nobuko Yoshida. Dynamic multirole session types. InProceedings of POPL'11, pages 435-446. ACM Press, 2011.","DOI":"10.1145\/1926385.1926435"},{"key":"10.2168\/LMCS-8(1:24)2012_FournetGonthier96","doi-asserted-by":"crossref","unstructured":"C\u00e9dric Fournet and Georges Gonthier. The reflexive CHAM and the join-calculus. InProceedings of POPL'96, pages 372-385. ACM Press, 1996.","DOI":"10.1145\/237721.237805"},{"key":"10.2168\/LMCS-8(1:24)2012_GM05","doi-asserted-by":"crossref","unstructured":"Blaise Genest and Anca Muscholl. Message sequence charts: A survey. InProceedings of ACSD'05, pages 2-4. IEEE Computer Society, 2005.","DOI":"10.1109\/ACSD.2005.25"},{"key":"10.2168\/LMCS-8(1:24)2012_GMP03","doi-asserted-by":"crossref","unstructured":"Blaise Genest, Anca Muscholl, and Doron Peled. Message sequence charts. InLectures on Concurrency and Petri Nets, LNCS 3098, pages 537-558. Springer, 2003.","DOI":"10.1007\/978-3-540-27755-2_15"},{"key":"10.2168\/LMCS-8(1:24)2012_HJ04","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.04.004"},{"key":"10.2168\/LMCS-8(1:24)2012_honda.vasconcelos.kubo:language-primitives","doi-asserted-by":"crossref","unstructured":"Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. InProceedings of ESOP'98, LNCS 1381, pages 22-138. Springer, 1998.","DOI":"10.1007\/BFb0053567"},{"key":"10.2168\/LMCS-8(1:24)2012_CHY08","doi-asserted-by":"crossref","unstructured":"Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. InProceedings of POPL'08, pages 273-284. ACM Press, 2008.","DOI":"10.1145\/1328438.1328472"},{"key":"10.2168\/LMCS-8(1:24)2012_casrl","doi-asserted-by":"crossref","unstructured":"Florent Jacquemard, Micha\u00ebl Rusinowitch, and Laurent Vigneron. Compiling and verifying security protocols. InProceedings of LPAR'00, LNCS 1955, pages 131-160. Springer, 2000.","DOI":"10.1007\/3-540-44404-1_10"},{"key":"10.2168\/LMCS-8(1:24)2012_LGMZ08","doi-asserted-by":"crossref","unstructured":"Ivan Lanese, Claudio Guidi, Fabrizio Montesi, and Gianluigi Zavattaro. Bridging the gap between interaction- and process-oriented choreographies. InProceedings of SEFM'08, pages 323-332. IEEE Computer Society, 2008.","DOI":"10.1109\/SEFM.2008.11"},{"key":"10.2168\/LMCS-8(1:24)2012_casper","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"Gavin Lowe","year":"1998","journal-title":"Journal of Computer Security"},{"key":"10.2168\/LMCS-8(1:24)2012_MD02","first-page":"16","volume":"4","author":"Jonathan K. Millen and Grit Denker","year":"2002","journal-title":"Journal of Telecommunications and Information Technology 4:16-27, 2002"},{"key":"10.2168\/LMCS-8(1:24)2012_Milner84","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90023-0"},{"key":"10.2168\/LMCS-8(1:24)2012_McK08","doi-asserted-by":"crossref","unstructured":"Jay A. McCarthy and Shriram Krishnamurthi. Cryptographic protocol explication and end-point projection. InProceedings of ESORICS'08, LNCS 5283, pages 533-547. Springer, 2008.","DOI":"10.1007\/978-3-540-88313-5_34"},{"key":"10.2168\/LMCS-8(1:24)2012_MPS98","doi-asserted-by":"crossref","unstructured":"Anca Muscholl, Doron Peled, and Zhendong Su. Deciding properties for message sequence charts. InProceedings of FOSSACS'98, LNCS 1378, pages 226-242. Springer, 1998.","DOI":"10.1007\/BFb0053553"},{"key":"10.2168\/LMCS-8(1:24)2012_MR97","doi-asserted-by":"crossref","unstructured":"Sjouke Mauw and Michel A. Reniers. High-level message sequence charts. InProceedings of SDL'97, pages 291-306. Elsevier, 1997.","DOI":"10.1016\/B978-044482816-3\/50020-4"},{"key":"10.2168\/LMCS-8(1:24)2012_Parikh66","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"10.2168\/LMCS-8(1:24)2012_QZ07","doi-asserted-by":"crossref","unstructured":"Zongyan Qiu, Xiangpeng Zhao, Chao Cai, and Hongli Yang. Towards the theoretical foundation of choreography. InProceedings of WWW'07, pages 973-982. ACM Press, 2007.","DOI":"10.1145\/1242572.1242704"},{"key":"10.2168\/LMCS-8(1:24)2012_Sch04","doi-asserted-by":"crossref","unstructured":"Philippe Schnoebelen. The verification of probabilistic lossy channel systems. InValidation of Stochastic Systems, LNCS 2925, pages 445-465. Springer, 2004.","DOI":"10.1007\/978-3-540-24611-4_13"},{"key":"10.2168\/LMCS-8(1:24)2012_THK","doi-asserted-by":"crossref","unstructured":"Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interaction-based language and its typing system. InProceedings of PARLE'94, LNCS 817, pages 398-413. Springer, 1994.","DOI":"10.1007\/3-540-58184-7_118"},{"key":"10.2168\/LMCS-8(1:24)2012_WSCDL","unstructured":"Web services choreography description language version 1.0. W3C Candidate Recommendation, available at http:\/\/www.w3.org\/TR\/ws-cdl-10\/, 2005. Nobuko Yoshida, Pierre-Malo Deni\u00e9lou, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. InProceedings of FOSSACS'10, LNCS 6014, pages 128-145. Springer, 2010."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/773\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/773\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:09:45Z","timestamp":1744067385000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/773"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,15]]},"references-count":43,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:24)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1203.0780","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.0780","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,15]]},"article-number":"773"}}