{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T07:38:12Z","timestamp":1774856292634,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T00:00:00Z","timestamp":1748390400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T00:00:00Z","timestamp":1748390400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100008394","name":"Natur og Univers, Det Frie Forskningsr\u00e5d","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008394","id-type":"DOI","asserted-by":"publisher"}]},{"name":"IT University"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Multiparty session types is a typing discipline used to write specifications, known as global types, for branching and recursive message-passing systems. A necessary operation on global types is projection to abstractions of local behaviour, called local types. Typically, this is a computable partial function that given a global type and a role erases all details irrelevant to this role. Computable projection functions in the literature are either unsound or too restrictive when dealing with recursion and branching. Recent work has taken a more general approach to projection defining it as a coinductive, but not computable, relation. Our work defines a new computable projection function that is sound and complete with respect to its coinductive counterpart and, hence, equally expressive. All results have been mechanised in the Coq proof assistant.<\/jats:p>","DOI":"10.1007\/s10817-025-09726-9","type":"journal-article","created":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T05:06:44Z","timestamp":1748408804000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Sound and Complete Projection for Global Types"],"prefix":"10.1007","volume":"69","author":[{"given":"Dawit","family":"Tirore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jesper","family":"Bengtson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Carbone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,28]]},"reference":[{"key":"9726_CR1","doi-asserted-by":"publisher","unstructured":"Asperti, A.: A compact proof of decidability for regular expression equivalence. In: Proceedings of ITP. LNCS, vol. 7406, pp. 283\u2013298. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_19","DOI":"10.1007\/978-3-642-32347-8_19"},{"key":"9726_CR2","doi-asserted-by":"publisher","unstructured":"Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: The Matita interactive theorem prover. In: Proceedings of CADE. LNCS, vol. 6803, pp. 64\u201369. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_7","DOI":"10.1007\/978-3-642-22438-6_7"},{"key":"9726_CR3","unstructured":"Barendregt, H.P.: The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics, vol. 103. North-Holland (1985)"},{"key":"9726_CR4","doi-asserted-by":"publisher","unstructured":"Bejleri, A., Yoshida, N.: Synchronous multiparty session types. In: Proceedings of PLACES. ENTCS, vol. 241, pp. 3\u201333. Elsevier (2008). https:\/\/doi.org\/10.1016\/j.entcs.2009.06.002","DOI":"10.1016\/j.entcs.2009.06.002"},{"key":"9726_CR5","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development - Coq\u2019Art: the calculus of inductive constructions. Texts in theoretical computer science. An EATCS Series. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9726_CR6","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: Proceedings of PLDI, pp. 237\u2013251. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454041","DOI":"10.1145\/3453483.3454041"},{"key":"9726_CR7","unstructured":"Coinductive types and corecursive functions. https:\/\/coq.inria.fr\/refman\/language\/core\/coinductive.html. Accessed May 2023"},{"key":"9726_CR8","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Certifying choreography compilation. In: Cerone, A., \u00d6lveczky, P.C. (eds.) Proceedings of ICTAC 2021. Lecture Notes in Computer Science, vol. 12819, pp. 115\u2013133. Springer (2021a). https:\/\/doi.org\/10.1007\/978-3-030-85315-0_8","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"9726_CR9","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.) Proceedings of ITP 2021. LIPIcs, vol. 193, pp. 15\u201311518. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021b). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.15","DOI":"10.4230\/LIPIcs.ITP.2021.15"},{"issue":"5","key":"9726_CR10","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"NG de Bruijn","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Math. (Proc.) 75(5), 381\u2013392 (1972). https:\/\/doi.org\/10.1016\/1385-7258(72)90034-0","journal-title":"Indagationes Math. (Proc.)"},{"key":"9726_CR11","doi-asserted-by":"publisher","unstructured":"Demangeon, R., Yoshida, N.: On the expressiveness of multiparty sessions. In: Proceedings of FSTTCS. LIPIcs, vol. 45, pp. 560\u2013574 (2015). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2015.560","DOI":"10.4230\/LIPIcs.FSTTCS.2015.560"},{"key":"9726_CR12","unstructured":"Eikelder, H.: Some algorithms to decide the equivalence of recursive types. https:\/\/pure.tue.nl\/ws\/files\/2150345\/9211264.pdf. Accessed May 2023 (1991)"},{"issue":"1","key":"9726_CR13","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1017\/S0956796809990268","volume":"20","author":"S Gay","year":"2010","unstructured":"Gay, S., Vasconcelos, V.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19\u201350 (2010). https:\/\/doi.org\/10.1017\/S0956796809990268","journal-title":"J. Funct. Program."},{"key":"9726_CR14","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.jlamp.2018.12.002","volume":"104","author":"S Ghilezan","year":"2019","unstructured":"Ghilezan, S., Jaksic, S., Pantovic, J., Scalas, A., Yoshida, N.: Precise subtyping for synchronous multiparty sessions. J. Logical Algebraic Methods Program. 104, 127\u2013173 (2019). https:\/\/doi.org\/10.1016\/j.jlamp.2018.12.002","journal-title":"J. Logical Algebraic Methods Program."},{"key":"9726_CR15","doi-asserted-by":"publisher","unstructured":"Glabbeek, R., H\u00f6fner, P., Horne, R.: Assuming just enough fairness to make session types complete for lock-freedom. In: Proceedings of LICS, pp. 1\u201313. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470531","DOI":"10.1109\/LICS52264.2021.9470531"},{"key":"9726_CR16","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the coq system (2016). https:\/\/inria.hal.science\/inria-00258384"},{"key":"9726_CR17","doi-asserted-by":"publisher","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Proceedings of ESOP. LNCS, vol. 1381, pp. 122\u2013138. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0053567","DOI":"10.1007\/BFb0053567"},{"key":"9726_CR18","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of POPL, pp. 273\u2013284. ACM (2008). https:\/\/doi.org\/10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"issue":"1","key":"9726_CR19","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/2827695","volume":"63","author":"K Honda","year":"2016","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9\u20131967 (2016). https:\/\/doi.org\/10.1145\/2827695","journal-title":"J. ACM"},{"key":"9726_CR20","doi-asserted-by":"publisher","unstructured":"Hur, C., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: Proceedings of POPL, pp. 193\u2013206. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429093","DOI":"10.1145\/2429069.2429093"},{"key":"9726_CR21","doi-asserted-by":"publisher","unstructured":"Jacobs, J., Balzer, S., Krebbers, R.: Multiparty GV: functional multiparty session types with certified deadlock freedom. Proceedings of the ACM on Programming Languages 6(ICFP), 466\u2013495 (2022) https:\/\/doi.org\/10.1145\/3547638","DOI":"10.1145\/3547638"},{"key":"9726_CR22","doi-asserted-by":"publisher","first-page":"347","DOI":"10.3233\/FI-2017-1473","volume":"150","author":"J-B Jeannin","year":"2017","unstructured":"Jeannin, J.-B., Kozen, D., Silva, A.: Cocaml: functional programming with regular coinductive types. Fund. Inform. 150, 347\u2013377 (2017). https:\/\/doi.org\/10.3233\/FI-2017-1473","journal-title":"Fund. Inform."},{"key":"9726_CR23","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"9726_CR24","doi-asserted-by":"publisher","first-page":"30","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, 30\u201313029 (2019). https:\/\/doi.org\/10.1145\/3290343","journal-title":"Proc. ACM Program. Lang."},{"key":"9726_CR25","unstructured":"Session types in programming languages: a collection of implementations. http:\/\/www.simonjf.com\/2016\/05\/28\/session-type-implementations.html. Accessed May 2023"},{"key":"9726_CR26","doi-asserted-by":"publisher","unstructured":"Sozeau, M., Mangin, C.: Equations reloaded: high-level dependently-typed functional programming and proving in coq. Proceedings of the ACM on Programming Languages 3(ICFP), 86\u201318629 (2019) https:\/\/doi.org\/10.1145\/3341690","DOI":"10.1145\/3341690"},{"key":"9726_CR27","doi-asserted-by":"publisher","unstructured":"Stark, K., Sch\u00e4fer, S., Kaiser, J.: Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In: Proceedings of CPP, pp. 166\u2013180. ACM (2019). https:\/\/doi.org\/10.1145\/3293880.3294101","DOI":"10.1145\/3293880.3294101"},{"key":"9726_CR28","unstructured":"The Coq development team: the Coq Proof Assistant. https:\/\/coq.inria.fr. Accessed May 2023"},{"key":"9726_CR29","doi-asserted-by":"publisher","unstructured":"Tirore, D.L., Bengtson, J., Carbone, M.: A sound and complete projection for global types. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bia\u0142ystok, Poland. LIPIcs, vol. 268, pp. 28\u201312819. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.28","DOI":"10.4230\/LIPICS.ITP.2023.28"},{"key":"9726_CR30","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Propositions as sessions. In: Thiemann, P., Findler, R.B. (eds.) ACM SIGPLAN International Conference on Functional Programming, ICFP\u201912, Copenhagen, Denmark, September 9-15, 2012, pp. 273\u2013286. ACM (2012). https:\/\/doi.org\/10.1145\/2364527.2364568","DOI":"10.1145\/2364527.2364568"},{"key":"9726_CR31","doi-asserted-by":"publisher","unstructured":"Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: two systems for higher-order session communication. In: Fern\u00e1ndez, M., Kirchner, C. (eds.) Proceedings of the First International Workshop on Security and Rewriting Techniques, SecReT@ICALP 2006, Venice, Italy, July 15, 2006. Electronic Notes in Theoretical Computer Science, vol. 171, pp. 73\u201393. Elsevier (2006). https:\/\/doi.org\/10.1016\/J.ENTCS.2007.02.056","DOI":"10.1016\/J.ENTCS.2007.02.056"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09726-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09726-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09726-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:04:06Z","timestamp":1750669446000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09726-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,28]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["9726"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09726-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,28]]},"assertion":[{"value":"28 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 April 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"14"}}