{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:07:51Z","timestamp":1784200071985,"version":"3.55.0"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work addresses this limitation by introducing probabilistic refinement session types which enable symbolic reasoning for concurrent probabilistic systems in a core calculus we call PReST. The type system is carefully designed to be a\n                    <jats:italic toggle=\"yes\">conservative extension<\/jats:italic>\n                    of refinement session types and supports both probabilistic and regular choice type operators. We also implement PReST in a prototype which we use for validating probabilistic concurrent programs. The added expressive power leads to significant challenges, in both the meta theory and implementation of PReST, particularly with type checking: it requires reconstructing intermediate types for channels when type checking probabilistic branching expressions. The theory handles this by semantically quantifying refinement variables in probabilistic typing rules, a deviation from standard refinement type systems. The implementation relies on a bi-directional type checker that uses an SMT solver to reconstruct the intermediate types minimizing annotation overhead and increasing usability. To guarantee that probabilistic processes are almost-surely terminating, we integrate cost analysis into our type system to obtain expected upper bounds on recursion depth. We evaluate PReST on a wide variety of benchmarks from 4 categories:\n                    <jats:italic toggle=\"yes\">(i)<\/jats:italic>\n                    randomized distributed protocols such as Itai and Rodeh\u2019s leader election, bounded retransmission, etc.,\n                    <jats:italic toggle=\"yes\">(ii)<\/jats:italic>\n                    parametric Markov chains such as random walks,\n                    <jats:italic toggle=\"yes\">(iii)<\/jats:italic>\n                    probabilistic analysis of concurrent data structures such as queues, and\n                    <jats:italic toggle=\"yes\">(iv)<\/jats:italic>\n                    distributions obtained by composing uniform distributions using operators like max and sum. Our experiments show that the PReST type checker scales to large programs with sophisticated probabilistic distributions.\n                  <\/jats:p>","DOI":"10.1145\/3729317","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1666-1691","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Probabilistic Refinement Session Types"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5234-8565","authenticated-orcid":false,"given":"Qiancheng","family":"Fu","sequence":"first","affiliation":[{"name":"Boston University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2459-1258","authenticated-orcid":false,"given":"Ankush","family":"Das","sequence":"additional","affiliation":[{"name":"Boston University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-7066","authenticated-orcid":false,"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"Boston University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.303.7"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15298-6_8"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0196-6774(90)90021-6"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785725"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.01"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78142-2_7"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51237-3_4"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"issue":"11","key":"e_1_3_2_15_1","article-title":"Linear Logic Propositions as Session Types.","volume":"760","author":"Caires Lu\u00eds","year":"2014","unstructured":"Lu\u00eds Caires, Frank Pfenning, and Bernardo Toninho. 2014. Linear Logic Propositions as Session Types. Mathematical Structures in Computer Science 760 (11 2014).","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.043"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"issue":"01","key":"e_1_3_2_19_1","article-title":"Dynamic Configuration of IPv4 Link-Local Addresses.","author":"Cheshire S.","year":"2005","unstructured":"S. Cheshire and Bernard Aboba. 2005. Dynamic Configuration of IPv4 Link-Local Addresses. IETF Internet Draft (01 2005).","journal-title":"IETF Internet Draft"},{"issue":"2011","key":"e_1_3_2_20_1","first-page":"2010","article-title":"The smt-libv2 language and tools: A tutorial.","author":"al David R Cok et","year":"2011","unstructured":"David R Cok et al. 2011. The smt-libv2 language and tools: A tutorial. Language c (2011), 2010\u20132011.","journal-title":"Language c"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2022.37"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80596-1"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00004"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.33"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Ankush Das and Frank Pfenning. 2020. Session Types with Arithmetic Refinements. (2020) 18pages. 512384 bytes https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2020.1310.4230\/LIPICS.CONCUR.2020.13","DOI":"10.4230\/LIPICS.CONCUR.2020.13"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414087"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571259"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Qiancheng Fu Ankush Das and Marco Gaboardi. 2025. Probabilistic Refinement Session Types (Artifact). https:\/\/doi.org\/10.5281\/zenodo.1515116110.5281\/zenodo.15151161","DOI":"10.5281\/zenodo.15151161"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Qiancheng Fu Ankush Das and Marco Gaboardi. 2025. Probabilistic Refinement Session Types (Companion Report). https:\/\/doi.org\/10.5281\/zenodo.1518526110.5281\/zenodo.15185261","DOI":"10.5281\/zenodo.15185261"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150.002"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_12"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_13"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167090"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689753"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58085-9_75"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46432-8_10"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.14"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.14"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90004-2"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0039071"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75307"},{"key":"e_1_3_2_57_1","first-page":"133","article-title":"On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In","author":"Lehmann Daniel","year":"1981","unstructured":"Daniel Lehmann and Michael O Rabin. 1981. On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. InProceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages.133\u2013138.","journal-title":"Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_4"},{"key":"e_1_3_2_59_1","unstructured":"Janine Lohse and Deepak Garg. 2024. An Iris for Expected Cost Analysis.arXiv:2406.00884 [cs.PL]https:\/\/arxiv.org\/abs\/2406.00884"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24611-4_11"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.31"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2006.07.015"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/293411.293778"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1123"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547643"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408992"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_72_1","unstructured":"Fangyi Zhou. 2019. Refinement Session Types.Imperial College London.Master\u2019s thesis."},{"key":"e_1_3_2_73_1","article-title":"Fluid Types: Statically Verified Distributed Protocols with Refinements. In","author":"Zhou Fangyi","year":"2019","unstructured":"Fangyi Zhou, Francisco Ferreira, Rumyuna Neykova, and Nobuko Yoshida. 2019. Fluid Types: Statically Verified Distributed Protocols with Refinements. In11th Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software.","journal-title":"11th Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729317","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:08:43Z","timestamp":1784196523000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729317"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":72,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729317"],"URL":"https:\/\/doi.org\/10.1145\/3729317","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}