{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T04:11:05Z","timestamp":1782879065428,"version":"3.54.5"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1350574, 1618059"],"award-info":[{"award-number":["1350574, 1618059"]}],"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":[[2021,1,4]]},"abstract":"<jats:p>Refinement types enable lightweight verification of functional programs. Algorithms for statically inferring refinement types typically work by reduction to solving systems of constrained Horn clauses extracted from typing derivations. An example is Liquid type inference, which solves the extracted constraints using predicate abstraction. However, the reduction to constraint solving in itself already signifies an abstraction of the program semantics that affects the precision of the overall static analysis. To better understand this issue, we study the type inference problem in its entirety through the lens of abstract interpretation. We propose a new refinement type system that is parametric with the choice of the abstract domain of type refinements as well as the degree to which it tracks context-sensitive control flow information. We then derive an accompanying parametric inference algorithm as an abstract interpretation of a novel data flow semantics of functional programs. We further show that the type system is sound and complete with respect to the constructed abstract semantics. Our theoretical development reveals the key abstraction steps inherent in refinement type inference algorithms. The trade-off between precision and efficiency of these abstraction steps is controlled by the parameters of the type system. Existing refinement type systems and their respective inference algorithms, such as Liquid types, are captured by concrete parameter instantiations. We have implemented our framework in a prototype tool and evaluated it for a range of new parameter instantiations (e.g., using octagons and polyhedra for expressing type refinements). The tool compares favorably against other existing tools. Our evaluation indicates that our approach can be used to systematically construct new refinement type inference algorithms that are both robust and precise.<\/jats:p>","DOI":"10.1145\/3434300","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Data flow refinement type inference"],"prefix":"10.1145","volume":"5","author":[{"given":"Zvonimir","family":"Pavlinovic","sequence":"first","affiliation":[{"name":"New York University, USA \/ Google, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yusen","family":"Su","sequence":"additional","affiliation":[{"name":"New York University, USA \/ University of Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[{"name":"New York University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32505-3_15"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico"},{"key":"e_1_2_1_4_1","unstructured":"Bruno Blanchet Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2007. A Static Analyzer for Large Safety-Critical Software. CoRR abs\/cs\/0701193 ( 2007 ). arXiv:cs\/0701193 http:\/\/arxiv.org\/abs\/cs\/0701193"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_20"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_8"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_21"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263744"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCL"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 and Xavier Rival. 2009. Why does Astr\u00e9e scale up? Formal Methods Syst. Des. 35 3 ( 2009 ) 229-264. https:\/\/doi.org\/10.1007\/s10703-009-0089-6 10.1007\/s10703-009-0089-6","DOI":"10.1007\/s10703-009-0089-6"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_16"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964025"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837631"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_16"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36384-X_13"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90026-Z"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"David Van Horn and Matthew Might. 2011. Abstracting abstract machines: a systematic approach to higher-order program analysis. Commun. ACM 54 9 ( 2011 ) 101-109. https:\/\/doi.org\/10.1145\/1995376.1995400 10.1145\/1995376.1995400","DOI":"10.1145\/1995376.1995400"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199536"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512672"},{"key":"e_1_2_1_30_1","article-title":"Higher-Order Minimal Function Graphs","volume":"1997","author":"Jones Neil D.","year":"1997","unstructured":"Neil D. Jones and Mads Rosendahl. 1997. Higher-Order Minimal Function Graphs. J. Funct. Log. Program. 1997, 2 ( 1997 ). http:\/\/danae.uni-muenster.de\/lehre\/kuchen\/JFLP\/articles\/1997\/A97-02\/ A97-02.html","journal-title":"J. Funct. Log. Program."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_13"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_21"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_18"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Nico","year":"2017","unstructured":"Nico Lehmann and \u00c9ric Tanter. 2017. Gradual refinement types. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 775-788. http:\/\/dl.acm.org\/citation.cfm?id= 3009856"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Jan Midtgaard. 2012. Control-flow analysis of functional programs. ACM Comput. Surv. 44 3 ( 2012 ) 10 : 1-10 : 33. https: \/\/doi.org\/10.1145\/2187671.2187672 10.1145\/2187671.2187672","DOI":"10.1145\/2187671.2187672"},{"key":"e_1_2_1_38_1","unstructured":"Antoine Min\u00e9. 2007. The Octagon Abstract Domain. CoRR abs\/cs\/0703084 ( 2007 ). arXiv:cs\/0703084 http:\/\/arxiv.org\/abs\/cs\/ 0703084"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56287-7_107"},{"key":"e_1_2_1_40_1","volume-title":"Static Analysis","author":"Monsuez Bruno","unstructured":"Bruno Monsuez. 1993. Polymorphic types and widening operators. In Static Analysis. Springer, 267-281."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60360-3_45"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/215465.215574"},{"key":"e_1_2_1_43_1","article-title":"Higher-Order Value Flow Graphs","volume":"5","author":"Mossin Christian","year":"1998","unstructured":"Christian Mossin. 1998. Higher-Order Value Flow Graphs. Nord. J. Comput. 5, 3 ( 1998 ), 214-234.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263745"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_21"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_47_1","volume-title":"Data Flow Refinement Type Inference. CoRR abs\/","author":"Pavlinovic Zvonimir","year":"2011","unstructured":"Zvonimir Pavlinovic, Yusen Su, and Thomas Wies. 2020. Data Flow Refinement Type Inference. CoRR abs\/ 2011.04876 ( 2020 ). arXiv: 2011.04876 http:\/\/arxiv.org\/abs\/ 2011.04876"},{"key":"e_1_2_1_48_1","volume-title":"Chien","author":"Plevyak John","year":"1995","unstructured":"John Plevyak and Andrew A. Chien. 1995. Iterative Flow Analysis."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Singh Gagandeep","year":"2017","unstructured":"Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2017. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 46-59. http:\/\/dl.acm.org\/citation.cfm?id= 3009885"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_25"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429081"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","unstructured":"Dimitrios Vardoulakis and Olin Shivers. 2011a. CFA2: a Context-Free Approach to Control-Flow Analysis. Log. Methods Comput. Sci. 7 2 ( 2011 ). https:\/\/doi.org\/10.2168\/LMCS-7( 2 :3) 2011 10.2168\/LMCS-7(2:3)2011","DOI":"10.2168\/LMCS-7("},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034785"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784745"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242756"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276502"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908110"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_19"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784766"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908125"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434300","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434300","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434300","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:29:16Z","timestamp":1781854156000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434300"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":67,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434300"],"URL":"https:\/\/doi.org\/10.1145\/3434300","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}