{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:25Z","timestamp":1775873545348,"version":"3.50.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"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-2120642, CNS-2155235, CCF-1918573, CCF-1911213, CCF-1955457"],"award-info":[{"award-number":["CNS-2120642, CNS-2155235, CCF-1918573, CCF-1911213, CCF-1955457"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101039196"],"award-info":[{"award-number":["101039196"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-19-1-2292"],"award-info":[{"award-number":["N00014-19-1-2292"]}],"id":[{"id":"10.13039\/100000006","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":[[2024,1,2]]},"abstract":"<jats:p>\n            Practical checkers based on refinement types use the combination of implicit semantic subtyping and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal metatheoretic accounting of the\n            <jats:italic toggle=\"yes\">soundness<\/jats:italic>\n            of refinement type systems using this combination has proved elusive. We present\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msub>\n                  <mml:mi>\u03bb<\/mml:mi>\n                  <mml:mrow>\n                    <mml:mi>R<\/mml:mi>\n                    <mml:mi>F<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:msub>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , a core refinement calculus that combines semantic subtyping and parametric polymorphism. We develop a metatheory for this calculus and prove soundness of the type system. Finally, we give two mechanizations of our metatheory. First, we introduce\n            <jats:italic toggle=\"yes\">data propositions<\/jats:italic>\n            , a novel feature that enables encoding derivation trees for inductively defined judgments as refined data types, and use them to show that L\n            <jats:sc>iquid<\/jats:sc>\n            H\n            <jats:sc>askell<\/jats:sc>\n            \u2019s refinement types can be used\n            <jats:italic toggle=\"yes\">for<\/jats:italic>\n            mechanization. Second, we mechanize our results in C\n            <jats:sc>oq<\/jats:sc>\n            , which comes with stronger soundness guarantees than L\n            <jats:sc>iquid<\/jats:sc>\n            H\n            <jats:sc>askell<\/jats:sc>\n            , thereby laying the foundations for mechanizing the metatheory\n            <jats:italic toggle=\"yes\">of<\/jats:italic>\n            L\n            <jats:sc>iquid<\/jats:sc>\n            H\n            <jats:sc>askell<\/jats:sc>\n            .\n          <\/jats:p>","DOI":"10.1145\/3632912","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2099-2128","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Mechanizing Refinement Types"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-8599-2237","authenticated-orcid":false,"given":"Michael H.","family":"Borkowski","sequence":"first","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0732-5476","authenticated-orcid":false,"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"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, La Jolla, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_2"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8425960"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8425176"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069793"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3546196.3550162"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110270"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046746"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029823"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607837"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-60750-100-8-73"},{"key":"e_1_3_1_19_1","volume-title":"Manifest Contracts","author":"Greenberg Michael","year":"2013","unstructured":"Michael Greenberg. 2013. Manifest Contracts. Ph.D. Dissertation. University of Pennsylvania. https:\/\/repository.upenn.edu\/edissertations\/468\/"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360592"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908091"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408988"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481853"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_1_26_1","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. STORM: Refinement Types for SecureWeb 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_27_1","volume-title":"2nd International Workshop on Coq for Programming Languages (CoqPL\u201916)","author":"Lehmann Nico","year":"2016","unstructured":"Nico Lehmann and \u00c9ric Tanter. 2016. Formalizing Simple Refinement Types in Coq. In 2nd International Workshop on Coq for Programming Languages (CoqPL\u201916). St. Petersburg, FL, USA."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_1_31_1","author":"Nipkow Tobias","year":"2002","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","journal-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic"},{"key":"e_1_3_1_32_1","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_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8141-3_34"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290388"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_1_37_1","volume":"2","author":"Pierce Benjamin C.","year":"2022","unstructured":"Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u0103t\u0103lin Hri\u0163cu, Vilhelm Sj\u00f6berg, Andrew Tolmach, and Brent Yorgey. 2022. Programming Language Foundations. Software Foundations, Vol. 2. Electronic textbook. https:\/\/softwarefoundations.cis.upenn.edu\/","journal-title":"Programming Language Foundations. Software Foundations"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58085-9_82"},{"key":"e_1_3_1_39_1","article-title":"Toward Hole-Driven Development with Liquid Haskell","author":"Redmond Patrick","year":"2021","unstructured":"Patrick Redmond, Gan Shen, and Lindsey Kuper. 2021. Toward Hole-Driven Development with Liquid Haskell. CoRR abs\/2110.04461 (2021). arXiv:2110.04461 https:\/\/arxiv.org\/abs\/2110.04461","journal-title":"CoRR abs\/2110.04461"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_41_1","unstructured":"Didier R\u00e9my. 2021. Type systems for programming languages. Course notes. https:\/\/www.doc.ic.ac.uk\/~svb\/TSfPL\/"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994594"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122963"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632912","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632912","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632912","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:11Z","timestamp":1751659631000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632912"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":51,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632912"],"URL":"https:\/\/doi.org\/10.1145\/3632912","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}