{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:42Z","timestamp":1775868582592,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T00:00:00Z","timestamp":1657843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["PTDC\/CCI-COM\/6453\/2020"],"award-info":[{"award-number":["PTDC\/CCI-COM\/6453\/2020"]}]},{"name":"LASIGE Research Unit","award":["UIDB\/00408\/2020 and UIDP\/00408\/2020"],"award-info":[{"award-number":["UIDB\/00408\/2020 and UIDP\/00408\/2020"]}]},{"name":"National Science Foundation","award":["1801369, 1845514, 1718276"],"award-info":[{"award-number":["1801369, 1845514, 1718276"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2022,9,30]]},"abstract":"<jats:p>Session types statically describe communication protocols between concurrent message-passing processes. Unfortunately, parametric polymorphism even in its restricted prenex form is not fully understood in the context of session types. In this article, we present the metatheory of session types extended with prenex polymorphism and, as a result, nested recursive datatypes. Remarkably, we prove that type equality is decidable by exhibiting a reduction to trace equivalence of deterministic first-order grammars. Recognizing the high theoretical complexity of the latter, we also propose a novel type equality algorithm and prove its soundness. We observe that the algorithm is surprisingly efficient and, despite its incompleteness, sufficient for all our examples. We have implemented our ideas by extending the Rast programming language with nested session types. We conclude with several examples illustrating the expressivity of our enhanced type system.<\/jats:p>","DOI":"10.1145\/3539656","type":"journal-article","created":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T12:29:14Z","timestamp":1657888154000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Nested Session Types"],"prefix":"10.1145","volume":"44","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2459-1258","authenticated-orcid":false,"given":"Ankush","family":"Das","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Cupertino, CA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1649-9953","authenticated-orcid":false,"given":"Henry","family":"Deyoung","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1547-0692","authenticated-orcid":false,"given":"Andreia","family":"Mordido","sequence":"additional","affiliation":[{"name":"Universidade de Lisboa, Lisboa, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8279-5817","authenticated-orcid":false,"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh"}]}],"member":"320","published-online":{"date-parts":[[2022,7,15]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_3"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015048"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.59.5"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:17)2012"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.11.006"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000803"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.162.4"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.06.002"},{"key":"e_1_3_3_14_2","article-title":"Rast Implementation","author":"Das Ankush","year":"2019","unstructured":"Ankush Das, Farzaneh Derakhshan, and Frank Pfenning. 2019. Rast Implementation. Retrieved November 11, 2019 from https:\/\/bitbucket.org\/fpfenning\/rast\/src\/master\/.","journal-title":"https:\/\/bitbucket.org\/fpfenning\/rast\/src\/master\/"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_7"},{"key":"e_1_3_3_16_2","unstructured":"Ankush Das Henry DeYoung Andreia Mordido and Frank Pfenning. 2021. Subtyping on nested polymorphic session types. arXiv:2103.15193 [cs.PL] (2021)."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236786"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.33"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.13"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414087"},{"key":"e_1_3_3_22_2","doi-asserted-by":"crossref","unstructured":"Farzaneh Derakhshan and Frank Pfenning. 2021. Circular proofs as session-typed processes: A local validity condition. arXiv:1908.01909 [cs.LO] (2021).","DOI":"10.46298\/lmcs-18(2:8)2022"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01443322"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90074-8"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_9"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006944"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014972"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.2172\/1562827"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/1778180.1778186"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39274-0_16"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003713"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_3_34_2","article-title":"Short decidability proof for DPDA language equivalence via 1st order grammar bisimilarity","volume":"1010","author":"Jan\u010dar Petr","year":"2010","unstructured":"Petr Jan\u010dar. 2010. Short decidability proof for DPDA language equivalence via 1st order grammar bisimilarity. CoRR abs\/1010.4760 (2010).","journal-title":"CoRR"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-009-9047-7"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_14"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40007-3_26"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068420000423"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1966.22"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12925-1_41"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.5555\/925926"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.08.001"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03741-2_10"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00027-0"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512765"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00389-3"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951926"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371135"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3539656","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3539656","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:03Z","timestamp":1750178283000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3539656"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,15]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9,30]]}},"alternative-id":["10.1145\/3539656"],"URL":"https:\/\/doi.org\/10.1145\/3539656","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,15]]},"assertion":[{"value":"2021-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}