{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:56:15Z","timestamp":1743069375488,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031773815"},{"type":"electronic","value":"9783031773822"}],"license":[{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"vor","delay-in-days":0,"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><jats:p>Multiparty Session Types (MPSTs) offer a structured way of specifying communication protocols and guarantee relevant communication properties, such as deadlock-freedom. In this paper, we extend a minimal MPST system with quantum data and operations, enabling the specification of quantum protocols. Quantum MPSTs (QMPSTs) provide a formal notation to describe quantum protocols, both at the abstract level of global types, describing which communications can take place in the system and their dependencies, and at the concrete level of local types and quantum processes, describing the expected behavior of each participant in the protocol. Type-checking relates these two levels formally, ensuring that processes behave as prescribed by the global type. Beyond usual communication properties, QMPSTs also allow us to prove that qubits are owned by a single process at any time, capturing the quantum no-cloning and no-deleting theorems. We use our approach to verify four quantum protocols from the literature, respectively Teleportation, Secret Sharing, Bit-Commitment, and Key Distribution.<\/jats:p>","DOI":"10.1007\/978-3-031-77382-2_22","type":"book-chapter","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T19:26:45Z","timestamp":1732562805000},"page":"385-403","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Quantum Multiparty Session Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2527-9995","authenticated-orcid":false,"given":"Ivan","family":"Lanese","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2030-8056","authenticated-orcid":false,"given":"Vikraman","family":"Choudhury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,26]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004, pp. 415\u2013425. IEEE (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319636","DOI":"10.1109\/LICS.2004.1319636"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Automated equivalence checking of concurrent quantum systems. ACM Trans. Comput. Log. 19(4), 28:1\u201328:32 (2018). https:\/\/doi.org\/10.1145\/3231597","DOI":"10.1145\/3231597"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-662-54434-1_3","volume-title":"Programming Languages and Systems","author":"R Atkey","year":"2017","unstructured":"Atkey, R.: Observed communication semantics for classical processes. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 56\u201382. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_3"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Barbanera, F., Dezani-Ciancaglini, M.: Partially typed multiparty sessions. In: 16th Interaction and Concurrency Experience, ICE 2023. EPTCS, pp. 15\u201334 (2023).https:\/\/doi.org\/10.4204\/EPTCS.383.2","DOI":"10.4204\/EPTCS.383.2"},{"key":"22_CR5","volume-title":"Dual intuitionistic linear logic","author":"A Barber","year":"1996","unstructured":"Barber, A., Plotkin, G.: Dual intuitionistic linear logic. University of Edinburgh, Laboratory for Foundations of Computer Science (1996)"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/j.tcs.2014.05.025","volume":"560","author":"CH Bennett","year":"2014","unstructured":"Bennett, C.H., Brassard, G.: Quantum cryptography: public key distribution and coin tossing. Theoret. Comput. Sci. 560, 7\u201311 (2014)","journal-title":"Theoret. Comput. Sci."},{"issue":"13","key":"22_CR7","doi-asserted-by":"publisher","first-page":"1895","DOI":"10.1103\/PhysRevLett.70.1895","volume":"70","author":"CH Bennett","year":"1993","unstructured":"Bennett, C.H., et al.: Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Phys. Rev. Lett. 70(13), 1895 (1993)","journal-title":"Phys. Rev. Lett."},{"key":"22_CR8","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.ic.2013.02.004","volume":"225","author":"M Bernardo","year":"2013","unstructured":"Bernardo, M., De Nicola, R., Loreti, M.: A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences. Inf. Comput. 225, 29\u201382 (2013)","journal-title":"Inf. Comput."},{"key":"22_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100844","volume":"131","author":"I Castellani","year":"2023","unstructured":"Castellani, I., Dezani-Ciancaglini, M., Giannini, P.: Event structure semantics for multiparty sessions. J. Logic. Algeb. Methods Program. 131, 100844 (2023). https:\/\/doi.org\/10.1016\/j.jlamp.2022.100844","journal-title":"J. Logic. Algeb. Methods Program."},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Ceragioli, L., et al.: Quantum bisimilarity via barbs and contexts: curbing the power of non-deterministic observers. Proc. ACM Program. Lang. 8(POPL), 1269\u20131297 (2024). https:\/\/doi.org\/10.1145\/3632885","DOI":"10.1145\/3632885"},{"key":"22_CR11","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.80.022339","volume":"80","author":"G Chiribella","year":"2009","unstructured":"Chiribella, G., D\u2019Ariano, G.M., Perinotti, P.: Theoretical framework for quantum networks. Phys. Rev. A 80, 022339 (2009). https:\/\/doi.org\/10.1103\/PhysRevA.80.022339","journal-title":"Phys. Rev. A"},{"key":"22_CR12","unstructured":"Choudhury, V.: Classical processes in modern dress (ST30 - SPLASH 2023). https:\/\/2023.splashcon.org\/details\/st-anniversary-30-papers\/9\/Classical-Processes-in-modern-dress"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"Dal Lago, U., Rioli, A.: Applicative bisimulation and quantum $$\\lambda $$-calculi. In: Dastani, M., Sirjani, M.: FSEN 2015. LNCS, vol. 9392, pp. 54\u201368. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-319-24644-4_4","DOI":"10.1007\/978-3-319-24644-4_4"},{"issue":"1","key":"22_CR14","first-page":"73","volume":"8","author":"TAS Davidson","year":"2012","unstructured":"Davidson, T.A.S., et al.: Model checking for communicating quantum processes. Int. J. Unconv. Comput. 8(1), 73\u201398 (2012)","journal-title":"Int. J. Unconv. Comput."},{"key":"22_CR15","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s11831-019-09372-6","volume":"28","author":"S Garhwal","year":"2021","unstructured":"Garhwal, S., Ghorani, M., Ahmad, A.: Quantum programming language: a systematic review of research topic and top cited languages. Archiv. Comput. Methods Eng. 28, 289\u2013310 (2021)","journal-title":"Archiv. Comput. Methods Eng."},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 145\u2013157. ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040318","DOI":"10.1145\/1040305.1040318"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"Gheri, L., et al.: Design-by-contract for flexible multiparty session protocols. In: Ali, K., Vitek, J.: 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), pp. 8:1\u20138:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.8","DOI":"10.4230\/LIPIcs.ECOOP.2022.8"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R., H\u00f6fner, P., Horne, R.: Assuming just enough fairness to make session types complete for lock-freedom. In: LICS, pp. 1\u201313. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470531","DOI":"10.1109\/LICS52264.2021.9470531"},{"key":"22_CR19","unstructured":"MISCGottesman, D., Chuang, I.: Quantum digital signatures. arXiv preprint arXiv:quantph\/0105032 (2001)"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Harvey, P., et al.: Multiparty session types for safe runtime adaptation in an actor language. In: ECOOP, LIPIcs, pp. 10:1\u201310:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2021.10","DOI":"10.4230\/LIPICS.ECOOP.2021.10"},{"issue":"3","key":"22_CR21","doi-asserted-by":"publisher","first-page":"1829","DOI":"10.1103\/PhysRevA.59.1829","volume":"59","author":"M Hillery","year":"1999","unstructured":"Hillery, M., Bu\u017eek, V., Berthiaume, A.: Quantum secret sharing. Phys. Rev. A 59(3), 1829 (1999)","journal-title":"Phys. Rev. A"},{"key":"22_CR22","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1\u20139:67 (2016). https:\/\/doi.org\/10.1145\/2827695","DOI":"10.1145\/2827695"},{"key":"22_CR23","doi-asserted-by":"publisher","unstructured":"Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: FASE. LNCS, vol. 10202, pp. 116\u2013133. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54494-5_7","DOI":"10.1007\/978-3-662-54494-5_7"},{"key":"22_CR24","doi-asserted-by":"publisher","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1\u20133:36 (2016). https:\/\/doi.org\/10.1145\/2873052","DOI":"10.1145\/2873052"},{"key":"22_CR25","unstructured":"Kavanagh, R.: A domain semantics for higher-order recursive processes. arXiv preprint arXiv:2002.01960 (2020)"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Lanese, I., Dal Lago, U., Choudhury, V.: Towards quantum multiparty session types. arXiv preprint arXiv:2409.11133 (2024)","DOI":"10.1007\/978-3-031-77382-2_22"},{"key":"22_CR27","unstructured":"Mlnarik, H.: Introduction to LanQ\u2013an Imperative quantum programming language (2006). https:\/\/lanq.sourceforge.net\/doc\/introToLanQ.pdf"},{"key":"22_CR28","unstructured":"Nielsen, M., Chuang, I.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010)"},{"key":"22_CR29","unstructured":"Papanikolaou, N.: Model checking quantum protocols. Ph.D. thesis, University of Warwick, Coventry (2009)"},{"key":"22_CR30","doi-asserted-by":"publisher","unstructured":"Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), 30:1\u201330:29 (2019). https:\/\/doi.org\/10.1145\/3290343","DOI":"10.1145\/3290343"},{"issue":"3","key":"22_CR31","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1017\/S0960129506005238","volume":"16","author":"P Selinger","year":"2006","unstructured":"Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. MSCS 16(3), 527\u2013552 (2006). https:\/\/doi.org\/10.1017\/S0960129506005238","journal-title":"MSCS"},{"key":"22_CR32","unstructured":"The Quantum Protocol Zoo (2024). https:\/\/wiki.veriqloud.fr\/"},{"key":"22_CR33","doi-asserted-by":"publisher","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: PPDP, pp. 161\u2013172. Association for Computing Machinery, New York (2011). https:\/\/doi.org\/10.1145\/2003476.2003499","DOI":"10.1145\/2003476.2003499"},{"key":"22_CR34","doi-asserted-by":"publisher","first-page":"802","DOI":"10.1038\/299802a0","volume":"299","author":"WK Wootters","year":"1982","unstructured":"Wootters, W.K., Zurek, W.H.: A single quantum cannot be cloned. Nature 299, 802\u2013803 (1982). https:\/\/doi.org\/10.1038\/299802a0","journal-title":"Nature"},{"key":"22_CR35","doi-asserted-by":"publisher","unstructured":"Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: ICDCIT. LNCS, vol. 11969, pp. 73\u201393. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-36987-3_5","DOI":"10.1007\/978-3-030-36987-3_5"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77382-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T23:55:38Z","timestamp":1733097338000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77382-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,26]]},"ISBN":["9783031773815","9783031773822"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77382-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,26]]},"assertion":[{"value":"26 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}