{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:04:25Z","timestamp":1781172265150,"version":"3.54.1"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            A binary session is a private communication channel that connects two processes, each adhering to a protocol description called\n            <jats:italic>session type<\/jats:italic>\n            . In this work, we study the first type system that ensures the\n            <jats:italic>fair termination<\/jats:italic>\n            of binary sessions. A session fairly terminates if all of the infinite executions admitted by its protocol are deemed unrealistic because they violate certain\n            <jats:italic>fairness assumptions<\/jats:italic>\n            . Fair termination entails the eventual completion of all pending input\/output actions, including those that depend on the completion of an unbounded number of other actions in possibly different sessions. This form of\n            <jats:italic>lock freedom<\/jats:italic>\n            allows us to address a large family of natural communication patterns that fall outside the scope of existing type systems. Our type system is also the first to adopt\n            <jats:italic>fair subtyping<\/jats:italic>\n            , a liveness-preserving refinement of the standard subtyping relation for session types that so far has only been studied theoretically. Fair subtyping is surprisingly subtle not only to characterize concisely but also to use appropriately, to the point that the type system must carefully account for all usages of fair subtyping to avoid compromising its liveness-preserving properties.\n          <\/jats:p>","DOI":"10.1145\/3498666","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Fair termination of binary sessions"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9515-5280","authenticated-orcid":false,"given":"Luca","family":"Ciccone","sequence":"first","affiliation":[{"name":"University of Turin, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9097-1297","authenticated-orcid":false,"given":"Luca","family":"Padovani","sequence":"additional","affiliation":[{"name":"University of Turin, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_2"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41642"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071370"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(2:10)2016"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.09.014"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_8"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007658"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14458-5_5"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.10.051"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(2:15)2009"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599437"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Luca Ciccone and Luca Padovani. 2021. FairCheck. https:\/\/github.com\/boystrange\/FairCheck  Luca Ciccone and Luca Padovani. 2021. FairCheck. https:\/\/github.com\/boystrange\/FairCheck","DOI":"10.1145\/3462304"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.125"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(1:26)2019"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.06.002"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.190.1"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04164-8_13"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.03.002"},{"key":"e_1_2_2_25_1","volume-title":"On the infinitary proof theory of logics with fixed points. (Th\u00e9orie de la d\u00e9monstration infinitaire pour les logiques \u00e0 points fixes). Ph. D. Dissertation","author":"Doumane Amina","unstructured":"Amina Doumane . 2017. On the infinitary proof theory of logics with fixed points. (Th\u00e9orie de la d\u00e9monstration infinitaire pour les logiques \u00e0 points fixes). Ph. D. Dissertation . Paris Diderot University , France. https:\/\/tel.archives-ouvertes.fr\/tel-01676953 Amina Doumane. 2017. On the infinitary proof theory of logics with fixed points. (Th\u00e9orie de la d\u00e9monstration infinitaire pour les logiques \u00e0 points fixes). Ph. D. Dissertation. Paris Diderot University, France. https:\/\/tel.archives-ouvertes.fr\/tel-01676953"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814277"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480895"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_5"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/800222.806752"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873052"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3171"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.03.004"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1745312.1745313"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0950-5849(89)90159-6"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00008921"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60084-1_112"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_34"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012951400022X"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43376-8_10"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.06.002"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_29"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3329125"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470531"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.004"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498666","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498666","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:27Z","timestamp":1750188627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498666"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498666"],"URL":"https:\/\/doi.org\/10.1145\/3498666","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}