{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T03:37:27Z","timestamp":1772077047842,"version":"3.50.1"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-2327336, CNS-2155235, CNS-2120642"],"award-info":[{"award-number":["CNS-2327336, CNS-2155235, CNS-2120642"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    We present\n                    <jats:italic toggle=\"yes\">Generic Refinement Types<\/jats:italic>\n                    : a way to write modular higher-order specifications that abstract invariants over function contracts, while preserving automatic SMT-decidable verification. We show how generic refinements let us write a variety of modular higher-order specifications, including specifications for Rust\u2019s traits which abstract over the concrete refinements that hold for different trait implementations. We formalize generic refinements in a core calculus and show how to synthesize the generic instantiations algorithmically at usage sites via a combination of syntactic unification and constraint solving. We give semantics to generic refinements via the intuition that they correspond to\n                    <jats:italic toggle=\"yes\">ghost parameters<\/jats:italic>\n                    , and we formalize this intuition via a type-preserving translation into the polymorphic contract calculus to establish the soundness of generic refinements. Finally, we evaluate generic refinements by implementing them in F\n                    <jats:sc>luk<\/jats:sc>\n                    and using it for two case studies. First, we show how generic refinements let us write modular specifications for Rust\u2019s vector indexing API that lets us statically verify the bounds safety of a variety of vector-manipulating benchmarks from the literature. Second, we use generic refinements to refine Rust\u2019s\n                    <jats:sc>diesel<\/jats:sc>\n                    ORM library to track the semantics of the database queries issued by client applications, and hence, statically enforce data-dependent access-control policies in several database-backed web applications.\n                  <\/jats:p>","DOI":"10.1145\/3704885","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1446-1474","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Generic Refinement Types"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6838-3714","authenticated-orcid":false,"given":"Nico","family":"Lehmann","sequence":"first","affiliation":[{"name":"University of California, San Diego, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6699-0430","authenticated-orcid":false,"given":"Cole","family":"Kurashige","sequence":"additional","affiliation":[{"name":"University of California, San Diego, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4608-7256","authenticated-orcid":false,"given":"Nikhil","family":"Akiti","sequence":"additional","affiliation":[{"name":"University of California, San Diego, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8638-6201","authenticated-orcid":false,"given":"Niroop","family":"Krishnakumar","sequence":"additional","affiliation":[{"name":"University of California, San Diego, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California, San Diego, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_1_3_2","unstructured":"Lennart Augustssonand Kent Petersson. 1994. Silly Type Families. (1994). https:\/\/web.cecs.pdx.edu\/~sheard\/papers\/silly.pdf."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_2"},{"key":"e_1_3_1_5_2","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2010","unstructured":"Yves Bertotand Pierre Castran. 2010. Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions (1st ed.). Springer Publishing Company, Incorporated."},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Aurel B\u00edl\u00fd Jonas Hansen Peter M\u00fcller and Alexander J. Summers. 2022. Compositional Reasoning for Side-effectful Iter- ators and Iterator Adapters. CoRR abs\/2210.09857 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2210.09857 10.48550\/ARXIV.2210.09857 arXiv:2210.09857","DOI":"10.48550\/ARXIV.2210.09857"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110270"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_9"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3610408"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_1_13_2","doi-asserted-by":"crossref","unstructured":"Lennard Gaher Michael Sammler Ralf Jung Robbert Krebbers and Derek Dreyer. 2023. Refined Rust: Towards high-assurance verification of unsafe Rust programs. https:\/\/people.mpi-sws.org\/~gaeher\/slides\/refinedrust_rw23.pdf","DOI":"10.1145\/3656422"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_1_18_2","first-page":"441","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Lehmann Nico","year":"2021","unstructured":"Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, and Ranjit Jhala. 2021. STORmml: Refinement Types for Secure Web Applications. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 441\u2013459. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/lehmann"},{"key":"e_1_3_1_19_2","doi-asserted-by":"crossref","unstructured":"Nico Lehmann Cole Kurashige Nikhil Akiti Niroop Krishnakumar and Ranjit Jhala. 2025. Generic Refinement Types- Technical Appendix. https:\/\/github.com\/FLUX-rs\/popl25","DOI":"10.1145\/3704885"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming Artificial Intelligence and Reasoning (LPAR). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Markus Wenzel and Lawrence C. Paulson. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. https:\/\/link.springer.com\/book\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_1_22_2","volume-title":"Towards a practical programming language based on dependent type theory","author":"Norell Ulf","year":"2007","unstructured":"Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph. D. Dissertation. Chalmers."},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2994594"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_1_27_2","doi-asserted-by":"crossref","unstructured":"The Diesel Core Team. 2024. Diesel: A Safe Extensible ORM and Query Builder for Rust. (2024). https:\/\/diesel.rs.","DOI":"10.22233\/20412495.0724.8"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784745"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/277652.277732"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","unstructured":"Christoph Zenger. 1997. Indexed types. Theor. Comput. Sci. 187 1\u20132 (nov 1997) 147\u2013165. https:\/\/doi.org\/10.1016\/S0304-3975(97)00062-5 10.1016\/S0304-3975(97)00062-5","DOI":"10.1016\/S0304-3975(97)00062-5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704885","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704885","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:33Z","timestamp":1770200073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704885"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704885"],"URL":"https:\/\/doi.org\/10.1145\/3704885","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}