{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T20:06:35Z","timestamp":1760731595873},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,5,27]],"date-time":"2023-05-27T00:00:00Z","timestamp":1685145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,5,27]],"date-time":"2023-05-27T00:00:00Z","timestamp":1685145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"University Library of Southern Denmark"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of choreographies typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of these proofs has led to important errors being found in published works. In this work, we formalise the theory of a choreographic programming language in Coq. Our development includes the basic properties of this language, a proof of its Turing completeness, a compilation procedure to a process language, and an operational characterisation of the correctness of this procedure. Our formalisation experience illustrates the benefits of using a theorem prover: we get both an additional degree of confidence from the mechanised proof, and a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.<\/jats:p>","DOI":"10.1007\/s10817-023-09665-3","type":"journal-article","created":{"date-parts":[[2023,5,27]],"date-time":"2023-05-27T03:31:18Z","timestamp":1685158278000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Formal Theory of Choreographic Programming"],"prefix":"10.1007","volume":"67","author":[{"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[]},{"given":"Fabrizio","family":"Montesi","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Peressotti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,5,27]]},"reference":[{"key":"9665_CR1","unstructured":"Albert, E., Lanese, I. (eds.): Formal Techniques for Distributed Objects, Components, and Systems\u201436th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, 6\u20139 June 2016, Proceedings. Lecture Notes in Computer Science, vol. 9688. Springer, Berlin (2016)"},{"issue":"2\u20133","key":"9665_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1561\/2500000031","volume":"3","author":"D Ancona","year":"2016","unstructured":"Ancona, D., Bono, V., Bravetti, M., Campos, J., Castagna, G., Deni\u00e9lou, P., Gay, S.J., Gesbert, N., Giachino, E., Hu, R., Johnsen, E.B., Martins, F., Mascardi, V., Montesi, F., Neykova, R., Ng, N., Padovani, L., Vasconcelos, V.T., Yoshida, N.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2\u20133), 95\u2013230 (2016)","journal-title":"Found. Trends Program. Lang."},{"key":"9665_CR3","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1016\/j.ic.2017.07.010","volume":"256","author":"M Bravetti","year":"2017","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: Undecidability of asynchronous session subtyping. Inf. Comput. 256, 300\u2013320 (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.07.010","journal-title":"Inf. Comput."},{"key":"9665_CR4","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.tcs.2018.02.010","volume":"722","author":"M Bravetti","year":"2018","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci. 722, 19\u201351 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2018.02.010","journal-title":"Theor. Comput. Sci."},{"key":"9665_CR5","unstructured":"Bravetti, M., Carbone, M., Lange, J., Yoshida, N., Zavattaro, G.: A sound algorithm for asynchronous session subtyping and its implementation. Log. Methods Comput. Sci. (2021). https:\/\/lmcs.episciences.org\/7238"},{"key":"9665_CR6","doi-asserted-by":"publisher","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) Proc. CONCUR. Lecture Notes in Computer Science, vol. 6269, pp. 222\u2013236. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"9665_CR7","doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: Giacobazzi, R., Cousot, R. (eds.) Procs. POPL, pp. 263\u2013274. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2429069.2429101","DOI":"10.1145\/2429069.2429101"},{"issue":"2","key":"9665_CR8","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/2220365.2220367","volume":"34","author":"M Carbone","year":"2012","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1-8:78 (2012). https:\/\/doi.org\/10.1145\/2220365.2220367","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9665_CR9","doi-asserted-by":"publisher","unstructured":"Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party sessions. In: Bruni, R., Dingel, J. (eds.) Procs. FORTE. LNCS, vol. 6722, pp. 1\u201328. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-21461-5_1","DOI":"10.1007\/978-3-642-21461-5_1"},{"key":"9665_CR10","doi-asserted-by":"publisher","unstructured":"Castro-Perez, D., Ferreira, F., Gheri, L., Yoshida, N.: Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In: Freund, S.N., Yahav, E. (eds.) Procs. PLDI, pp. 237\u2013251. ACM, New York (2021). https:\/\/doi.org\/10.1145\/3453483.3454041","DOI":"10.1145\/3453483.3454041"},{"key":"9665_CR11","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F.: Choreographies in practice. In: Albert, E., Lanese, I. (eds.): Formal Techniques for Distributed Objects, Components, and Systems\u201436th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, 6\u20139 June 2016, Proceedings, pp. 114\u2013123. https:\/\/doi.org\/10.1007\/978-3-319-39570-8_8","DOI":"10.1007\/978-3-319-39570-8_8"},{"key":"9665_CR12","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F.: On asynchrony and choreographies. In: Bartoletti, M., Bocchi, L., Henrio, L., Knight, S. (eds.) Procs. ICE, EPTCS, vol. 261, pp. 76\u201390 (2017). https:\/\/doi.org\/10.4204\/EPTCS.261.8","DOI":"10.4204\/EPTCS.261.8"},{"key":"9665_CR13","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F.: Procedural choreographic programming. In: Bouajjani, A., Silva, A. (eds.) Procs. FORTE. Lecture Notes in Computer Science, vol. 10321, pp. 92\u2013107. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-60225-7_7","DOI":"10.1007\/978-3-319-60225-7_7"},{"key":"9665_CR14","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Lugovi\u0107, L., Montesi, F.: Certified compilation of choreographies with HACC. CoRR. (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.03972","DOI":"10.48550\/arXiv.2303.03972"},{"key":"9665_CR15","unstructured":"Cruz-Filipe, L., Montesi, F., Rasmussen, R.R.: Keep me out of the loop: a more flexible choreographic projection. Submitted for publication"},{"key":"9665_CR16","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.tcs.2019.07.005","volume":"802","author":"L Cruz-Filipe","year":"2020","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","journal-title":"Theor. Comput. Sci."},{"key":"9665_CR17","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F.: Now it compiles! certified automatic repair of uncompilable protocols. CoRR. (2023). https:\/\/doi.org\/10.48550\/arXiv.2302.14622","DOI":"10.48550\/arXiv.2302.14622"},{"key":"9665_CR18","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Larsen, K.S., Montesi, F.: The paths to choreography extraction. In: Foundations of Software Science and Computation Structures\u201420th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22\u201329, 2017, Proceedings, LNCS, vol. 10203, pp. 424\u2013440. https:\/\/doi.org\/10.1007\/978-3-662-54458-7_25","DOI":"10.1007\/978-3-662-54458-7_25"},{"key":"9665_CR19","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Choreographies in Coq. In: TYPES 2019, Abstracts (2019). Extended abstract"},{"key":"9665_CR20","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Certifying choreography compilation. In: Cerone, A., \u00d6lveczky, P.C. (eds.) Procs. ICTAC, LNCS, vol. 12819, pp. 115\u2013133. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-85315-0_8","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"9665_CR21","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Formalising a Turing-complete choreographic language in Coq. In: Cohen, L., Kaliszyk, C. (eds.) Procs. ITP, LIPIcs, vol. 193, pp. 15:1\u201315:18. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Wadern (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.15","DOI":"10.4230\/LIPIcs.ITP.2021.15"},{"key":"9665_CR22","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: A formal theory of choreographic programming in Coq (2022). https:\/\/doi.org\/10.5281\/zenodo.7773479","DOI":"10.5281\/zenodo.7773479"},{"key":"9665_CR23","unstructured":"Dalla\u00a0Preda, M., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies: Theory and implementation. Log. Methods Comput. Sci. (2017). https:\/\/doi.org\/10.23638\/LMCS-13(2:1)2017"},{"key":"9665_CR24","doi-asserted-by":"crossref","unstructured":"Esparza, J., Murawski, A.S. (eds.): Foundations of Software Science and Computation Structures\u201420th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, 22\u201329 April 2017, Proceedings, LNCS, vol. 10203 (2017)","DOI":"10.1007\/978-3-662-54458-7"},{"key":"9665_CR25","doi-asserted-by":"publisher","unstructured":"Finkel, A., Lozes, \u00c9.: Synchronizability of communicating finite state machines is not decidable. In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl, A. (eds.) Procs. ICALP, LIPIcs, vol.\u00a080, pp. 122:1\u2013122:14. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Wadern (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2017.122","DOI":"10.4230\/LIPIcs.ICALP.2017.122"},{"issue":"1","key":"9665_CR26","doi-asserted-by":"publisher","first-page":"158","DOI":"10.4230\/DagRep.7.1.158","volume":"7","author":"SJ Gay","year":"2017","unstructured":"Gay, S.J., Vasconcelos, V.T., Wadler, P., Yoshida, N.: Theory and applications of behavioural types (Dagstuhl seminar 17051). Dagstuhl Rep. 7(1), 158\u2013189 (2017). https:\/\/doi.org\/10.4230\/DagRep.7.1.158","journal-title":"Dagstuhl Rep."},{"key":"9665_CR27","doi-asserted-by":"publisher","unstructured":"Giallorenzo, S., Lanese, I., Russo, D.: Chip: A choreographic integration process. In: Panetto, H., Debruyne, C., Proper, H.A., Ardagna, C.A., Roman, D., Meersman, R. (eds.) Procs. OTM, part II. Lecture Notes in Computer Science, vol. 11230, pp. 22\u201340. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-030-02671-4_2","DOI":"10.1007\/978-3-030-02671-4_2"},{"key":"9665_CR28","unstructured":"Giallorenzo, S., Montesi, F., Peressotti, M.: Choreographies as objects. CoRR. (2020). https:\/\/arxiv.org\/abs\/2005.09520"},{"issue":"POPL","key":"9665_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498684","volume":"6","author":"AK Hirsch","year":"2022","unstructured":"Hirsch, A.K., Garg, D.: Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang. 6(POPL), 1\u201327 (2022). https:\/\/doi.org\/10.1145\/3498684","journal-title":"Proc. ACM Program. Lang."},{"key":"9665_CR30","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM (2016). https:\/\/doi.org\/10.1145\/2827695. Also: POPL, pp. 273\u2013284 (2008)","DOI":"10.1145\/2827695"},{"issue":"1","key":"9665_CR31","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2873052","volume":"49","author":"H H\u00fcttel","year":"2016","unstructured":"H\u00fcttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deni\u00e9lou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1-3:36 (2016). https:\/\/doi.org\/10.1145\/2873052","journal-title":"ACM Comput. Surv."},{"key":"9665_CR32","unstructured":"Intl. Telecommunication Union: Recommendation Z.120: Message Sequence Chart (1996)"},{"issue":"ICFP","key":"9665_CR33","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1145\/3547638","volume":"6","author":"J Jacobs","year":"2022","unstructured":"Jacobs, J., Balzer, S., Krebbers, R.: Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang. 6(ICFP), 466\u2013495 (2022). https:\/\/doi.org\/10.1145\/3547638","journal-title":"Proc. ACM Program. Lang."},{"key":"9665_CR34","volume-title":"Introduction to Metamathematics","author":"SC Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics, vol. 1. North-Holland, Amsterdam (1952)"},{"key":"9665_CR35","doi-asserted-by":"publisher","unstructured":"Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Esparza, J., Murawski, A.S. (eds.) Foundations of Software Science and Computation Structures\u201420th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, 22\u201329 April 2017, Proceedings, pp. 441\u2013457. https:\/\/doi.org\/10.1007\/978-3-662-54458-7_26","DOI":"10.1007\/978-3-662-54458-7_26"},{"key":"9665_CR36","doi-asserted-by":"publisher","unstructured":"Lluch-Lafuente, A., Nielson, F., Nielson, H.R.: Discretionary information flow control for interaction-oriented specifications. In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C.L. (eds.) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science, vol. 9200, pp. 427\u2013450. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-23165-5_20","DOI":"10.1007\/978-3-319-23165-5_20"},{"key":"9665_CR37","doi-asserted-by":"publisher","unstructured":"L\u00f3pez, H.A., Heussen, K.: Choreographing cyber-physical distributed control systems for the energy sector. In: Seffah, A., Penzenstadler, B., Alves, C., Peng, X. (eds.) Procs. SAC, pp. 437\u2013443. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3019612.3019656","DOI":"10.1145\/3019612.3019656"},{"key":"9665_CR38","doi-asserted-by":"publisher","unstructured":"L\u00f3pez, H.A., Nielson, F., Nielson, H.R.: Enforcing availability in failure-aware communicating systems. In: Albert, E., Lanese, I. (eds.) Formal Techniques for Distributed Objects, Components, and Systems\u201436th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, 6\u20139 June 2016, Proceedings, pp. 195\u2013211. https:\/\/doi.org\/10.1007\/978-3-319-39570-8_13","DOI":"10.1007\/978-3-319-39570-8_13"},{"key":"9665_CR39","doi-asserted-by":"publisher","unstructured":"Maksimovic, P., Schmitt, A.: HOCore in Coq. In: Urban, C., Zhang, X. (eds.) Procs. ITP. Lecture Notes in Computer Science, vol. 9236, pp. 278\u2013293. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_19","DOI":"10.1007\/978-3-319-22102-1_19"},{"key":"9665_CR40","unstructured":"Montesi, F.: Choreographic programming. Ph.D. Thesis, IT University of Copenhagen (2013). http:\/\/www.fabriziomontesi.com\/files\/choreographic_programming.pdf"},{"key":"9665_CR41","doi-asserted-by":"publisher","DOI":"10.1017\/9781108981491","volume-title":"Introduction to Choreographies","author":"F Montesi","year":"2023","unstructured":"Montesi, F.: Introduction to Choreographies. Cambridge University Press, Cambridge (2023)"},{"issue":"12","key":"9665_CR42","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"RM Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978). https:\/\/doi.org\/10.1145\/359657.359659","journal-title":"Commun. ACM"},{"key":"9665_CR43","unstructured":"Object\u00a0Management Group: Business Process Model and Notation. http:\/\/www.omg.org\/spec\/BPMN\/2.0\/ (2011)"},{"key":"9665_CR44","doi-asserted-by":"publisher","unstructured":"Pohjola, J.\u00c5., G\u00f3mez-Londo\u00f1o, A., Shaker, J., Norrish, M.: Kalas: a verified, end-to-end compiler for a choreographic language. In: Andronick, J., de\u00a0Moura, L. (eds.) Procs. ITP, LIPIcs, vol. 237, pp. 27:1\u201327:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Wadern (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.27","DOI":"10.4230\/LIPIcs.ITP.2022.27"},{"issue":"POPL","key":"9665_CR45","doi-asserted-by":"publisher","first-page":"30:1","DOI":"10.1145\/3290343","volume":"3","author":"A Scalas","year":"2019","unstructured":"Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), 30:1-30:29 (2019). https:\/\/doi.org\/10.1145\/3290343","journal-title":"Proc. ACM Program. Lang."},{"key":"9665_CR46","unstructured":"W3C: WS Choreography Description Language. http:\/\/www.w3.org\/TR\/ws-cdl-10\/ (2004)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09665-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09665-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09665-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,21]],"date-time":"2023-06-21T11:05:17Z","timestamp":1687345517000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09665-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,27]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6]]}},"alternative-id":["9665"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09665-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,27]]},"assertion":[{"value":"7 September 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 April 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"21"}}