{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T17:34:19Z","timestamp":1787506459335,"version":"build-2736575974"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100008433","name":"Comunidad de Madrid","doi-asserted-by":"publisher","award":["S2018\/TCS-4339"],"award-info":[{"award-number":["S2018\/TCS-4339"]}],"id":[{"id":"10.13039\/501100008433","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/P00587X\/1"],"award-info":[{"award-number":["EP\/P00587X\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2020,1]]},"abstract":"<jats:p>Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this article, we show how Liquid Haskell can also be used to reason about program efficiency in the same setting. We use the system's existing verification machinery to ensure that the results of our cost analysis are valid, together with custom invariants for particular program contexts to ensure that the results of our analysis are precise. To illustrate our approach, we analyse the efficiency of a wide range of popular data structures and algorithms, and in doing so, explore various notions of resource usage. Our experience is that reasoning about efficiency in Liquid Haskell is often just as simple as reasoning about correctness, and that the two can naturally be combined.<\/jats:p>","DOI":"10.1145\/3371092","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T14:45:25Z","timestamp":1576853125000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Liquidate your assets: reasoning about resource usage in liquid Haskell"],"prefix":"10.1145","volume":"4","author":[{"given":"Martin A. T.","family":"Handley","sequence":"first","affiliation":[{"name":"University of Nottingham, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"University of Nottingham, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Alejandro Aguirre Gilles Barthe Marco Gaboardi Deepak Garg and Pierre-Yves Strub. 2017. A Relational Logic for Higher-Order Programs. In ICFP. ACM.  Alejandro Aguirre Gilles Barthe Marco Gaboardi Deepak Garg and Pierre-Yves Strub. 2017. A Relational Logic for Higher-Order Programs. In ICFP. ACM.","DOI":"10.1145\/3110265"},{"key":"e_1_2_2_2_1","volume-title":"Theoretical Computer Science","author":"Aspinall David"},{"key":"e_1_2_2_3_1","volume-title":"Amortised Resource Analysis with Separation Logic","author":"Atkey Robert"},{"key":"e_1_2_2_4_1","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves"},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Rod M Burstall and John Darlington. 1977. A Transformation System for Developing Recursive Programs. In JACM. ACM.  Rod M Burstall and John Darlington. 1977. A Transformation System for Developing Recursive Programs. In JACM. ACM.","DOI":"10.1145\/321992.321996"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Ezgi \u00c7i\u00e7ek Gilles Barthe Marco Gaboardi Deepak Garg and Jan Hoffmann. 2017. Relational Cost Analysis. In POPL. ACM.  Ezgi \u00c7i\u00e7ek Gilles Barthe Marco Gaboardi Deepak Garg and Jan Hoffmann. 2017. Relational Cost Analysis. In POPL. ACM.","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Ezgi \u00c7i\u00e7ek Weihao Qu Gilles Barthe Marco Gaboardi and Deepak Garg. 2019. Bidirectional Type Checking for Relational Properties. In PLDI. ACM.  Ezgi \u00c7i\u00e7ek Weihao Qu Gilles Barthe Marco Gaboardi and Deepak Garg. 2019. Bidirectional Type Checking for Relational Properties. In PLDI. ACM.","DOI":"10.1145\/3314221.3314603"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Karl Crary and Stephnie Weirich. 2000. Resource Bound Certification. In POPL. ACM.  Karl Crary and Stephnie Weirich. 2000. Resource Bound Certification. In POPL. ACM.","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In POPL. ACM.  Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In POPL. ACM.","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_2_11_1","volume-title":"Handley and Niki Vazou","author":"Martin","year":"2019"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann Klaus Aehlig and Martin Hofmann. 2011. Multivariate Amortized Resource Analysis. In POPL. ACM.  Jan Hoffmann Klaus Aehlig and Martin Hofmann. 2011. Multivariate Amortized Resource Analysis. In POPL. ACM.","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","volume-title":"Resource Aware ML","author":"Hoffmann Jan","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","volume-title":"Automatic Static Cost Analysis for Parallel Programs","author":"Hoffmann Jan","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Steffen Jost. 2003. Static Prediction of Heap Space Usage for First-Order Functional Programs. In POPL. ACM.  Martin Hofmann and Steffen Jost. 2003. Static Prediction of Heap Space Usage for First-Order Functional Programs. In POPL. ACM.","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"John Hughes Lars Pareto and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In POPL. ACM.  John Hughes Lars Pareto and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In POPL. ACM.","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_2_17_1","unstructured":"Guoliang Jin Linhai Song Xiaoming Shi Joel Scherpelz and Shan Lu. 2012. Understanding and Detecting Real-World Performance Bugs. In PLDI. ACM.  Guoliang Jin Linhai Song Xiaoming Shi Joel Scherpelz and Shan Lu. 2012. Understanding and Detecting Real-World Performance Bugs. In PLDI. ACM."},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Steffen Jost Kevin Hammond Hans-Wolfgang Loidl and Martin Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In POPL. ACM.  Steffen Jost Kevin Hammond Hans-Wolfgang Loidl and Martin Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In POPL. ACM.","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_2_19_1","volume-title":"Journal of Automated Reasoning","author":"Jost Steffen"},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","unstructured":"Ravichandhran Madhavan Sumith Kulal and Viktor Kuncak. 2017. Contract-Based Resource Verification for Higher-Order Functions with Memoization. In POPL. ACM.  Ravichandhran Madhavan Sumith Kulal and Viktor Kuncak. 2017. Contract-Based Resource Verification for Higher-Order Functions with Memoization. In POPL. ACM.","DOI":"10.1145\/3009837.3009874"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Jay McCarthy Burke Fetscher Max S. New Daniel Feltey and Robert Findler. 2017. A Coq Library for Internal Verification of Running-Times. Science of Computer Programming.  Jay McCarthy Burke Fetscher Max S. New Daniel Feltey and Robert Findler. 2017. A Coq Library for Internal Verification of Running-Times. Science of Computer Programming.","DOI":"10.1007\/978-3-319-29604-3_10"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Andrew Moran and David Sands. 1999. Improvement in a Lazy Context: An Operational Theory for Call-By-Need. In POPL. ACM.  Andrew Moran and David Sands. 1999. Improvement in a Lazy Context: An Operational Theory for Call-By-Need. In POPL. ACM.","DOI":"10.1145\/292540.292547"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","volume-title":"Dependently Typed Programming in Agda","author":"Norell Ulf","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","volume-title":"Purely Functional Data Structures","author":"Okasaki Chris","DOI":"10.1017\/CBO9780511530104"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Ivan Radi\u010dek Gilles Barthe Marco Gaboardi Deepak Garg and Florian Zuleger. 2018. Monadic Refinements for Relational Cost Analysis. In POPL. ACM.  Ivan Radi\u010dek Gilles Barthe Marco Gaboardi Deepak Garg and Florian Zuleger. 2018. Monadic Refinements for Relational Cost Analysis. In POPL. ACM.","DOI":"10.1145\/3158124"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"David Sands. 1995. Total Correctness by Local Improvement in Program Transformation. In POPL. ACM.  David Sands. 1995. Total Correctness by Local Improvement in Program Transformation. In POPL. ACM.","DOI":"10.1145\/199448.199485"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","volume-title":"Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs","author":"Vasconcelos Pedro B","DOI":"10.1007\/978-3-540-27861-0_6"},{"key":"e_1_2_2_29_1","unstructured":"Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph.D. Dissertation. UC San Diego.  Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph.D. Dissertation. UC San Diego."},{"key":"e_1_2_2_30_1","volume-title":"Theorem Proving For All: Equational Reasoning in Liquid Haskell. In Haskell Symposium.","author":"Vazou Niki","year":"2018"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","volume-title":"Abstract Refinement Types","author":"Vazou Niki","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Niki Vazou Eric L Seidel Ranjit Jhala Dimitrios Vytiniotis and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In ICFP. ACM.  Niki Vazou Eric L Seidel Ranjit Jhala Dimitrios Vytiniotis and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In ICFP. ACM.","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_33_1","volume-title":"Refinement Reflection: Complete Verification with SMT. POPL.","author":"Vazou Niki","year":"2017"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Peng Wang Di Wang and Adam Chlipala. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. OOPSLA.  Peng Wang Di Wang and Adam Chlipala. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. OOPSLA.","DOI":"10.1145\/3133903"},{"key":"e_1_2_2_35_1","unstructured":"Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In POPL. ACM.  Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In POPL. ACM."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371092","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371092","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:43Z","timestamp":1750259143000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371092"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371092"],"URL":"https:\/\/doi.org\/10.1145\/3371092","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}