{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:37:38Z","timestamp":1770755858429,"version":"3.50.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>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 conservative extension 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, both in 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: (i) randomized distributed protocols such as Itai and Rodeh's leader election, bounded retransmission, etc., (ii) parametric Markov chains such as random walks, (iii) probabilistic analysis of concurrent data structures such as queues, and (iv) 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.<\/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":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2459-1258","authenticated-orcid":false,"given":"Ankush","family":"Das","sequence":"additional","affiliation":[{"name":"Boston University, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-7066","authenticated-orcid":false,"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"Boston University, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.303.7"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15298-6_8"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0196-6774(90)90021-6"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785725"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.019"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_2_2_11_1","volume-title":"Towards Probabilistic Session-Type Monitoring","author":"Burl\u00f2 Christian Bartolo","unstructured":"Christian Bartolo Burl\u00f2, Adrian Francalanza, Alceste Scalas, Catia Trubiani, and Emilio Tuosto. 2021. Towards Probabilistic Session-Type Monitoring. In Coordination Models and Languages, Ferruccio Damiani and Ornela Dardha (Eds.). Springer International Publishing, Cham. 106\u2013120. isbn:978-3-030-78142-2"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51237-3_4"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_2_14_1","first-page":"11","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 (2014), 11.","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.043"},{"key":"e_1_2_2_16_1","volume-title":"Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s","author":"Chatterjee Krishnendu","unstructured":"Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham. 3\u201322. isbn:978-3-319-41528-4"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"S. Cheshire and Bernard Aboba. 2005. Dynamic Configuration of IPv4 Link-Local Addresses. IETF Internet Draft 01.","DOI":"10.17487\/rfc3927"},{"key":"e_1_2_2_19_1","volume-title":"The smt-libv2 language and tools: A tutorial. Language c","author":"Cok David R","year":"2010","unstructured":"David R Cok. 2011. The smt-libv2 language and tools: A tutorial. Language c, 2010\u20132011."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2022.37"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80596-1"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00004"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.33"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","unstructured":"Ankush Das and Frank Pfenning. 2020. Session Types with Arithmetic Refinements. 18 pages 512384 bytes. issn:1868-8969 https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2020.13 10.4230\/LIPICS.CONCUR.2020.13","DOI":"10.4230\/LIPICS.CONCUR.2020.13"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414087"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571259"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_29_1","volume-title":"A Storm is Coming: A Modern Probabilistic Model Checker","author":"Dehnert Christian","unstructured":"Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. 2017. A Storm is Coming: A Modern Probabilistic Model Checker. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 592\u2013600. isbn:978-3-319-63390-9"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/113446.113468"},{"key":"e_1_2_2_32_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.15151161 10.5281\/zenodo.15151161","DOI":"10.5281\/zenodo.15151161"},{"key":"e_1_2_2_33_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.15185261 10.5281\/zenodo.15185261","DOI":"10.5281\/zenodo.15185261"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150.002"},{"key":"e_1_2_2_36_1","volume-title":"A Probabilistic Applied Pi\u2013Calculus","author":"Goubault-Larrecq Jean","unstructured":"Jean Goubault-Larrecq, Catuscia Palamidessi, and Angelo Troina. 2007. A Probabilistic Applied Pi\u2013Calculus. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 175\u2013190. isbn:978-3-540-76637-7"},{"key":"e_1_2_2_37_1","volume-title":"Gunter","author":"Griffith Dennis","year":"2013","unstructured":"Dennis Griffith and Elsa L. Gunter. 2013. LiquidPi: Inferrable Dependent Session Types. In NASA Formal Methods, Guillaume Brat, Neha Rungta, and Arnaud Venet (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 185\u2013197. isbn:978-3-642-38088-4"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167090"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689753"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"L. Helmink M. P. A. Sellink and F. W. Vaandrager. 1994. Proof-checking a data link protocol. In Types for Proofs and Programs Henk Barendregt and Tobias Nipkow (Eds.). Springer Berlin Heidelberg Berlin Heidelberg. 127\u2013165. isbn:978-3-540-48440-0","DOI":"10.1007\/3-540-58085-9_75"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46432-8_10"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_2_44_1","volume-title":"Language primitives and type discipline for structured communication-based programming","author":"Honda Kohei","unstructured":"Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. In Programming Languages and Systems, Chris Hankin (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 122\u2013138. isbn:978-3-540-69722-0"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.14"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2020.14"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90004-2"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0039071"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_51_1","volume-title":"Weakest Precondition Reasoning for Expected Run\u2013Times of Probabilistic Programs","author":"Kaminski Benjamin Lucien","unstructured":"Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run\u2013Times of Probabilistic Programs. In Programming Languages and Systems, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 364\u2013389. isbn:978-3-662-49498-1"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"e_1_2_2_54_1","volume-title":"Verification of Probabilistic Real-Time Systems","author":"Kwiatkowska Marta","unstructured":"Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 585\u2013591. isbn:978-3-642-22110-1"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75307"},{"key":"e_1_2_2_56_1","volume-title":"Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 133\u2013138","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. In Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 133\u2013138."},{"key":"e_1_2_2_57_1","volume-title":"Automated Expected Amortised Cost Analysis of\u00a0Probabilistic Data Structures","author":"Leutgeb Lorenz","unstructured":"Lorenz Leutgeb, Georg Moser, and Florian Zuleger. 2022. Automated Expected Amortised Cost Analysis of\u00a0Probabilistic Data Structures. In Computer Aided Verification, Sharon Shoham and Yakir Vizel (Eds.). Springer International Publishing, Cham. 70\u201391. isbn:978-3-031-13188-2"},{"key":"e_1_2_2_58_1","unstructured":"Janine Lohse and Deepak Garg. 2024. An Iris for Expected Cost Analysis. arxiv:2406.00884. arxiv:2406.00884"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24611-4_11"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.31"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2006.07.015"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/293411.293778"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1995.1123"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547643"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408992"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_2_2_70_1","volume-title":"Dependent Types in Practical Programming. In Conference Record of the 26th Symposium on Principles of Programming Languages (POPL","author":"Xi Hongwei","year":"1999","unstructured":"Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In Conference Record of the 26th Symposium on Principles of Programming Languages (POPL 1999), A. Aiken (Ed.). ACM Press, San Antonio, Texas, USA. 214\u2013227."},{"key":"e_1_2_2_71_1","volume-title":"Refinement Session Types. Master\u2019s thesis","author":"Zhou Fangyi","unstructured":"Fangyi Zhou. 2019. Refinement Session Types. Master\u2019s thesis. Imperial College London."},{"key":"e_1_2_2_72_1","volume-title":"Fluid Types: Statically Verified Distributed Protocols with Refinements. In 11th Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software.","author":"Zhou Fangyi","year":"2019","unstructured":"Fangyi Zhou, Francisco Ferreira, Rumyana Neykova, and Nobuko Yoshida. 2019. Fluid Types: Statically Verified Distributed Protocols with Refinements. In 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":[[2025,7,16]],"date-time":"2025-07-16T06:08:14Z","timestamp":1752646094000},"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"}}]}}