{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T18:01:33Z","timestamp":1755799293332,"version":"3.40.3"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031626968"},{"type":"electronic","value":"9783031626975"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-62697-5_9","type":"book-chapter","created":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T21:01:23Z","timestamp":1718053283000},"page":"149-158","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["The Concurrent Calculi Formalisation Benchmark"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9479-2632","authenticated-orcid":false,"given":"Marco","family":"Carbone","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6939-4189","authenticated-orcid":false,"given":"David","family":"Castro-Perez","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8494-7696","authenticated-orcid":false,"given":"Francisco","family":"Ferreira","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3191-7722","authenticated-orcid":false,"given":"Lorenzo","family":"Gheri","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3651-8314","authenticated-orcid":false,"given":"Frederik Krogsdal","family":"Jacobsen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0942-4777","authenticated-orcid":false,"given":"Alberto","family":"Momigliano","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9097-1297","authenticated-orcid":false,"given":"Luca","family":"Padovani","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1153-6164","authenticated-orcid":false,"given":"Alceste","family":"Scalas","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1997-5161","authenticated-orcid":false,"given":"Dawit","family":"Tirore","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2057-0495","authenticated-orcid":false,"given":"Martin","family":"Vassor","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3925-8557","authenticated-orcid":false,"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6153-2955","authenticated-orcid":false,"given":"Daniel","family":"Zackon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,11]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1017\/S0956796819000170","volume":"29","author":"A Abel","year":"2019","unstructured":"Abel, A., et al.: POPLMark reloaded: mechanizing proofs by logical relations. J. Funct. Program. 29, 19 (2019). https:\/\/doi.org\/10.1017\/S0956796819000170","journal-title":"J. Funct. Program."},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: POPL 2013: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 27\u201338. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2429069.2429075","DOI":"10.1145\/2429069.2429075"},{"issue":"1","key":"9_CR3","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/S10817-020-09553-0","volume":"65","author":"G Ambal","year":"2021","unstructured":"Ambal, G., Lenglet, S., Schmitt, A.: HO$$\\pi $$ in Coq. J. Autom. Reason. 65(1), 75\u2013124 (2021). https:\/\/doi.org\/10.1007\/S10817-020-09553-0","journal-title":"J. Autom. Reason."},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"BE Aydemir","year":"2005","unstructured":"Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50\u201365. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_4"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: a framework for mobile processes with nominal data and logic. Log. Methods Comput. Sci. 7 (2011). https:\/\/doi.org\/10.2168\/LMCS-7(1:11)2011","DOI":"10.2168\/LMCS-7(1:11)2011"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Bengtson, J., Parrow, J.: Formalising the pi-calculus using nominal logic. Log. Methods Comput. Sci. 5 (2009). https:\/\/doi.org\/10.2168\/LMCS-5(2:16)2009","DOI":"10.2168\/LMCS-5(2:16)2009"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-015-9336-2","volume":"56","author":"J Bengtson","year":"2016","unstructured":"Bengtson, J., Parrow, J., Weber, T.: Psi-calculi in Isabelle. J. Autom. Reason. 56, 1\u201347 (2016). https:\/\/doi.org\/10.1007\/s10817-015-9336-2","journal-title":"J. Autom. Reason."},{"key":"9_CR8","unstructured":"Bock, P., Murawska, A., Bruni, A., Sch\u00fcrmann, C.: Representing session types (2016). https:\/\/pure.itu.dk\/en\/publications\/representing-session-types, in Dale Miller\u2019s Festschrift"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107\u2013121. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_9"},{"issue":"51\u201352","key":"9_CR10","doi-asserted-by":"publisher","first-page":"4399","DOI":"10.1016\/j.tcs.2010.09.010","volume":"411","author":"L Caires","year":"2010","unstructured":"Caires, L., Vieira, H.T.: Conversation types. Theor. Comput. Sci. 411(51\u201352), 4399\u20134440 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.09.010","journal-title":"Theor. Comput. Sci."},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL 2013: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 263\u2013274. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2429069.2429101","DOI":"10.1145\/2429069.2429101"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-030-45237-7_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Castro","year":"2020","unstructured":"Castro, D., Ferreira, F., Yoshida, N.: EMTST: engineering the meta-theory of session types. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12079, pp. 278\u2013285. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_17"},{"key":"9_CR13","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: PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 237\u2013251. ACM, New York (2021). https:\/\/doi.org\/10.1145\/3453483.3454041","DOI":"10.1145\/3453483.3454041"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Chaudhuri, K., Cimini, M., Miller, D.: A lightweight formalization of the metatheory of bisimulation-up-to. In: Leroy, X., Tiu, A. (eds.) CPP 2015: Proceedings of the 4th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 157\u2013166. ACM (2015). https:\/\/doi.org\/10.1145\/2676724.2693170","DOI":"10.1145\/2676724.2693170"},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.tcs.2019.02.023","volume":"781","author":"K Chaudhuri","year":"2019","unstructured":"Chaudhuri, K., Lima, L., Reis, G.: Formalized meta-theory of sequent calculi for linear logics. Theor. Comput. Sci. 781, 24\u201338 (2019). https:\/\/doi.org\/10.1016\/j.tcs.2019.02.023","journal-title":"Theor. Comput. Sci."},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Ciccone, L., Padovani, L.: A dependently typed linear $$\\pi $$-calculus in Agda. In: PPDP 2020: 22nd International Symposium on Principles and Practice of Declarative Programming, pp. 8:1\u20138:14. ACM (2020). https:\/\/doi.org\/10.1145\/3414080.3414109","DOI":"10.1145\/3414080.3414109"},{"key":"9_CR17","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.) ITP 2021: Proceedings of the 12th International Conference on Interactive Theorem Proving. Leibniz International Proceedings in Informatics, Dagstuhl, Germany, vol.\u00a0193, pp. 15:1\u201315:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.15","DOI":"10.4230\/LIPIcs.ITP.2021.15"},{"issue":"1\u20134","key":"9_CR18","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/S10817-018-9458-4","volume":"61","author":"L Czajka","year":"2018","unstructured":"Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1\u20134), 423\u2013453 (2018). https:\/\/doi.org\/10.1007\/S10817-018-9458-4","journal-title":"J. Autom. Reason."},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-32347-8_11","volume-title":"Interactive Theorem Proving","author":"NA Danielsson","year":"2012","unstructured":"Danielsson, N.A.: Bag equivalence via a proof-relevant membership relation. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 149\u2013165. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_11"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.ic.2017.06.002","volume":"256","author":"O Dardha","year":"2017","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253\u2013286 (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.06.002","journal-title":"Inf. Comput."},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Derakhshan, F., Pfenning, F.: Circular proofs as session-typed processes: a local validity condition. Log. Methods Comput. Sci. 18(2) (2022). https:\/\/doi.org\/10.46298\/LMCS-18(2:8)2022","DOI":"10.46298\/LMCS-18(2:8)2022"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/3-540-44929-9_30","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"J Despeyroux","year":"2000","unstructured":"Despeyroux, J.: A higher-order specification of the $$\\pi $$-calculus. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 425\u2013439. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44929-9_30"},{"issue":"3","key":"9_CR23","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1017\/S0960129521000323","volume":"31","author":"AP Felty","year":"2021","unstructured":"Felty, A.P., Olarte, C., Xavier, B.: A focused linear logical framework and its application to metatheory of object logics. Math. Struct. Comput. Sci. 31(3), 312\u2013340 (2021). https:\/\/doi.org\/10.1017\/S0960129521000323","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"9_CR24","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/J.IC.2010.09.004","volume":"209","author":"A Gacek","year":"2011","unstructured":"Gacek, A., Miller, D., Nadathur, G.: Nominal abstraction. Inf. Comput. 209(1), 48\u201373 (2011). https:\/\/doi.org\/10.1016\/J.IC.2010.09.004","journal-title":"Inf. Comput."},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49099-X_6","volume-title":"Programming Languages and Systems","author":"S Gay","year":"1999","unstructured":"Gay, S., Hole, M.: Types and subtypes for client-server interactions. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 74\u201390. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49099-X_6"},{"issue":"2\u20133","key":"9_CR26","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/S00236-005-0177-Z","volume":"42","author":"SJ Gay","year":"2005","unstructured":"Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2\u20133), 191\u2013225 (2005). https:\/\/doi.org\/10.1007\/S00236-005-0177-Z","journal-title":"Acta Informatica"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Thiemann, P., Vasconcelos, V.T.: Duality of session types: the final cut. In: Proceedings of the PLACES 2020. Electronic Proceedings in Theoretical Computer Science, vol.\u00a0314, pp. 23\u201333. Open Publishing Association (2020). https:\/\/doi.org\/10.4204\/eptcs.314.3","DOI":"10.4204\/eptcs.314.3"},{"issue":"9","key":"9_CR28","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1016\/j.ic.2010.05.002","volume":"208","author":"D Gorla","year":"2010","unstructured":"Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031\u20131053 (2010). https:\/\/doi.org\/10.1016\/j.ic.2010.05.002","journal-title":"Inf. Comput."},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"Hirsch, A.K., Garg, D.: Pirouette: Higher-order typed functional choreographies. Proc. ACM Program. Lang. 6 (2022). https:\/\/doi.org\/10.1145\/3498684","DOI":"10.1145\/3498684"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0028392","volume-title":"Theorem Proving in Higher Order Logics","author":"D Hirschkoff","year":"1997","unstructured":"Hirschkoff, D.: A full formalisation of $$\\pi $$-calculus theory in the calculus of constructions. In: Gunter, E.L., Felty, A. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 153\u2013169. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0028392"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1) (2016). https:\/\/doi.org\/10.1145\/2827695","DOI":"10.1145\/2827695"},{"issue":"2","key":"9_CR32","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: $$\\pi $$-calculus in (co)inductive-type theory. Theor. Comput. Sci. 253(2), 239\u2013285 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00095-5","journal-title":"Theor. Comput. Sci."},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Horne, R., Padovani, L.: A logical account of subtyping for session types. In: Castellani, I., Scalas, A. (eds.) Proceedings of the 14th Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software. EPTCS, vol.\u00a0378, pp. 26\u201337. Open Publishing Association (2023). https:\/\/doi.org\/10.4204\/EPTCS.378.3","DOI":"10.4204\/EPTCS.378.3"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Hur, C.K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: POPL 2013: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 193\u2013206. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2429069.2429093","DOI":"10.1145\/2429069.2429093"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-69407-6_33","volume-title":"Logic and Theory of Algorithms","author":"T Kahsai","year":"2008","unstructured":"Kahsai, T., Miculan, M.: Implementing Spi calculus using nominal techniques. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 294\u2013305. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69407-6_33"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-319-22102-1_19","volume-title":"Interactive Theorem Proving","author":"P Maksimovi\u0107","year":"2015","unstructured":"Maksimovi\u0107, P., Schmitt, A.: HOCore in Coq. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 278\u2013293. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_19"},{"issue":"1","key":"9_CR37","first-page":"50","volume":"1","author":"TF Melham","year":"1994","unstructured":"Melham, T.F.: A mechanized theory of the $$\\pi $$-calculus in HOL. Nordic J. Comput. 1(1), 50\u201376 (1994)","journal-title":"Nordic J. Comput."},{"issue":"9","key":"9_CR38","doi-asserted-by":"publisher","first-page":"1541","DOI":"10.1017\/S096012951700010X","volume":"28","author":"R Perera","year":"2018","unstructured":"Perera, R., Cheney, J.: Proof-relevant $$\\pi $$-calculus: a constructive account of concurrency and causality. Math. Struct. Comput. Sci. 28(9), 1541\u20131577 (2018). https:\/\/doi.org\/10.1017\/S096012951700010X","journal-title":"Math. Struct. Comput. Sci."},{"volume-title":"Advanced Topics in Types and Programming Languages","year":"2004","key":"9_CR39","unstructured":"Pierce, B.C. (ed.): Advanced Topics in Types and Programming Languages. MIT Press, London (2004)"},{"key":"9_CR40","doi-asserted-by":"publisher","unstructured":"Pohjola, J., 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.) ITP 2022: Proceedings of the 13th International Conference on Interactive Theorem Proving. Leibniz International Proceedings in Informatics, Dagstuhl, Germany, vol.\u00a0237, pp. 27:1\u201327:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.27","DOI":"10.4230\/LIPIcs.ITP.2022.27"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Pous, D.: Coinduction all the way up. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, NY, USA, 5\u20138 July 2016, pp. 307\u2013316. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934564","DOI":"10.1145\/2933575.2934564"},{"key":"9_CR42","doi-asserted-by":"publisher","unstructured":"Rouvoet, A., Poulsen, C.B., Krebbers, R., Visser, E.: Intrinsically-typed definitional interpreters for linear, session-typed languages. In: Proceedings of the CPP 2020, pp. 284\u2013298. ACM (2020). https:\/\/doi.org\/10.1145\/3372885.3373818","DOI":"10.1145\/3372885.3373818"},{"key":"9_CR43","volume-title":"The $$\\pi $$-calculus: A Theory of Mobile Processes","author":"D Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: The $$\\pi $$-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)"},{"key":"9_CR44","doi-asserted-by":"publisher","unstructured":"Sano, C., Kavanagh, R., Pientka, B.: Mechanizing session-types using a structural view: enforcing linearity without linearity. Proc. ACM Program. Lang. 7(OOPSLA), 235:374\u2013235:399 (2023). https:\/\/doi.org\/10.1145\/3622810","DOI":"10.1145\/3622810"},{"key":"9_CR45","doi-asserted-by":"publisher","unstructured":"Scalas, A., Yoshida, N.: Less is more: Multiparty session types revisited. Proc. ACM Program. Lang. 3 (2019). https:\/\/doi.org\/10.1145\/3290343","DOI":"10.1145\/3290343"},{"key":"9_CR46","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-540-71070-7_28","volume-title":"Automated Reasoning","author":"A Schack-Nielsen","year":"2008","unstructured":"Schack-Nielsen, A., Sch\u00fcrmann, C.: Celf \u2013 a logical framework for deductive and concurrent systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 320\u2013326. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_28"},{"key":"9_CR47","doi-asserted-by":"publisher","unstructured":"Thiemann, P.: Intrinsically-typed mechanized semantics for session types. In: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3354166.3354184","DOI":"10.1145\/3354166.3354184"},{"key":"9_CR48","doi-asserted-by":"publisher","unstructured":"Tiu, A., Miller, D.: Proof search specifications of bisimulation and modal logics for the $$\\pi $$-calculus. ACM Trans. Comput. Logic 11(2) (2010). https:\/\/doi.org\/10.1145\/1656242.1656248","DOI":"10.1145\/1656242.1656248"},{"key":"9_CR49","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.ic.2012.05.002","volume":"217","author":"VT Vasconcelos","year":"2012","unstructured":"Vasconcelos, V.T.: Fundamentals of session types. Inf. Comput. 217, 52\u201370 (2012). https:\/\/doi.org\/10.1016\/j.ic.2012.05.002","journal-title":"Inf. Comput."},{"key":"9_CR50","doi-asserted-by":"publisher","unstructured":"Xia, L.Y., et al.: Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4 (2019). https:\/\/doi.org\/10.1145\/3371119","DOI":"10.1145\/3371119"},{"key":"9_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-030-78089-0_9","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"U Zalakain","year":"2021","unstructured":"Zalakain, U., Dardha, O.: $$\\pi $$ with leftovers: a mechanisation in Agda. In: Peters, K., Willemse, T.A.C. (eds.) FORTE 2021. LNCS, vol. 12719, pp. 157\u2013174. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_9"}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-62697-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T21:02:17Z","timestamp":1718053337000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-62697-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031626968","9783031626975"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-62697-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"11 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Alberto Momigliano is a member of the Gruppo Nazionale Calcolo Scientifico-Istituto Nazionale di Alta Matematica (GNCS-INdAM).","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"COORDINATION","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Coordination Models and Languages","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Groningen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","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":"17 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}