{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:52:02Z","timestamp":1790927522582,"version":"4.1.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"horizoneurope","award":["GA 101039196"],"award-info":[{"award-number":["GA 101039196"]}]},{"name":"mciu","award":["CEX2024-001471-M"],"award-info":[{"award-number":["CEX2024-001471-M"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,4,10]]},"abstract":"<jats:p>\n                    Refinement types often use SMT solvers to automate program verification. However, since SMT solvers are first-order, verification of properties that requires higher-order reasoning is not possible. Proof by Logical Evaluation (PLE) is an algorithm that provides a layer between refinement types and SMT solvers that permits symbolic evaluation of functions, but it lacks support for higher-order reasoning. We introduce PLEX, an extension to PLE, that supports\n                    <jats:italic toggle=\"yes\">\u03b7<\/jats:italic>\n                    -expansions,\n                    <jats:italic toggle=\"yes\">\u03b2<\/jats:italic>\n                    -reductions, and dependent pattern matching. We prove that PLEX is sound and terminating, describe its implementation in Liquid Haskell, and evaluate it on examples that make essential use of higher-order data, and as such they cannot be handled by PLE. The new PLEX algorithm bridges the gap between higher-order languages and first-order SMT solvers via refinement types.\n                  <\/jats:p>","DOI":"10.1145\/3798248","type":"journal-article","created":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T14:33:43Z","timestamp":1775831623000},"page":"1321-1347","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["PLEX: Normalization for Refinement Types"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-8919-3022","authenticated-orcid":false,"given":"Alessio","family":"Ferrarini","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"},{"name":"Universidad Polit\u00e9cnica de Madrid, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0295-7944","authenticated-orcid":false,"given":"Wouter","family":"Swierstra","sequence":"additional","affiliation":[{"name":"Utrecht University, Utrecht, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000180"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_2"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632912"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236770"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"A. Ferrarini N. Vazou and W. Swierstra. 2026. Artifact for \u201cPLEX: Normalization for Refinement Types\u201d. https:\/\/doi.org\/10.5281\/zenodo.19126672 10.5281\/zenodo.19126672","DOI":"10.5281\/zenodo.19126672"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/113446.113468"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00132"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_27"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360592"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_1"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"K.M.R. Leino. 2010. Dafny: an automatic program verifier for functional correctness. In Logic for Programming Artificial Intelligence and Reasoning. 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_19_1","doi-asserted-by":"publisher","unstructured":"K.M.R. Leino and C. Pit-Claudel. 2016. Trigger Selection Strategies to Stabilize Program Verifiers. In CAV. https:\/\/doi.org\/10.1007\/978-3-319-41528-4_20 10.1007\/978-3-319-41528-4_20","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"C. McBride. 2002. Elimination with a Motive. In Types for Proofs and Programs. https:\/\/doi.org\/10.1007\/3-540-45842-5_13 10.1007\/3-540-45842-5_13","DOI":"10.1007\/3-540-45842-5_13"},{"key":"e_1_3_1_21_1","unstructured":"C. McBride. 2012. A Polynomial Testing Principle. PDF. https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/PolyTest.pdf"},{"key":"e_1_3_1_22_1","unstructured":"A. D. Miller. 1991. Unification of Simply Typed Lambda-Terms as Logic Programming. In International Logic Programming Conference. https:\/\/doi.org\/20.500.14332\/7376"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-98682-6_11"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"G. Nelson and D. C. Oppen. 1979. Simplification by Cooperating Decision Procedures. (1979). https:\/\/doi.org\/10.1145\/357073.357079 10.1145\/357073.357079","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"T. Nipkow and C. Prehofer. 1998. Higher-Order Rewriting and Equational Reasoning. In Automated Deduction \u2014 A Basis for Applications. Volume I: Foundations. https:\/\/doi.org\/10.1007\/3-540-48685-2_17 10.1007\/3-540-48685-2_17","DOI":"10.1007\/3-540-48685-2_17"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473587"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"J. C. Reynolds. 1972. Definitional interpreters for higher-order programming languages. In ACM Annual Conference. https:\/\/doi.org\/10.1145\/800194.805852 10.1145\/800194.805852","DOI":"10.1145\/800194.805852"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375602"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_19"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000101"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676974"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000084"},{"key":"e_1_3_1_36_1","unstructured":"The Agda Development Team. 2024. Agda wiki. https:\/\/wiki.portal.chalmers.se\/agda\/Main\/HomePage"},{"key":"e_1_3_1_37_1","unstructured":"The Rocq Development Team. 2024. The Rocq Reference Manual \u2013 Release 8.19.0. https:\/\/coq.inria.fr\/doc\/V8.19.0\/refman"},{"key":"e_1_3_1_38_1","unstructured":"C. Thierry. 1992. Pattern Matching with Dependent Types. (1992). https:\/\/wonks.github.io\/type-theory-reading-group\/papers\/proc92-coquand.pdf"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.18"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3546189.3549919"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628161"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/277652.277732"},{"key":"e_1_3_1_44_1","unstructured":"Z3 Team. 2025. Z3 Guide - Lambdas. https:\/\/microsoft.github.io\/z3guide\/docs\/logic\/Lambdas\/. Accessed: 2025-06-20."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3798248","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T11:18:36Z","timestamp":1790421516000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3798248"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,10]]},"references-count":43,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2026,4,10]]}},"alternative-id":["10.1145\/3798248"],"URL":"https:\/\/doi.org\/10.1145\/3798248","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,10]]},"assertion":[{"value":"2025-10-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}