{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:35:53Z","timestamp":1774838153372,"version":"3.50.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Comunidad de Madrid BLOQUESCM","award":["S2018\/TCS-4339"],"award-info":[{"award-number":["S2018\/TCS-4339"]}]},{"name":"Attractio?n de Talento","award":["2019-T2\/TIC-13455"],"award-info":[{"award-number":["2019-T2\/TIC-13455"]}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-C-0022"],"award-info":[{"award-number":["FA8750-16-C-0022"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100008536","name":"Amazon Web Services","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008536","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation","award":["CNS-1563722, CNS-1801545"],"award-info":[{"award-number":["CNS-1563722, CNS-1801545"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>\n            This paper presents an extension to Liquid Haskell that facilitates stating and semi-automatically proving properties of typeclasses. Liquid Haskell augments Haskell with\n            <jats:italic>refinement types<\/jats:italic>\n            \u2014our work allows such types to be attached to typeclass method declarations, and ensures that instance implementations respect these types. The engineering of this extension is a modular interaction between GHC, the Glasgow Haskell Compiler, and Liquid Haskell\u2019s core proof infrastructure. The design sheds light on the interplay between modular proofs and typeclass resolution, which in Haskell is coherent by default (meaning that resolution always selects the same implementation for a particular instantiating type), but in other dependently typed languages is not.\n          <\/jats:p>\n          <jats:p>We demonstrate the utility of our extension by using Liquid Haskell to modularly verify that 34 instances satisfy the laws of five standard typeclasses.<\/jats:p>\n          <jats:p>\n            More substantially, we implement a framework for programming distributed applications based on\n            <jats:italic>replicated data types<\/jats:italic>\n            (RDTs). We define a typeclass whose Liquid Haskell type captures the mathematical properties RDTs should satisfy; prove in Liquid Haskell that these properties are sufficient to ensure that replicas\u2019 states converge despite out-of-order update delivery; implement (and prove correct) several instances of our RDT typeclass; and use them to build two realistic applications, a multi-user calendar event planner and a collaborative text editor.\n          <\/jats:p>","DOI":"10.1145\/3428284","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Verifying replicated data types with typeclass refinements in Liquid Haskell"],"prefix":"10.1145","volume":"4","author":[{"given":"Yiyun","family":"Liu","sequence":"first","affiliation":[{"name":"University of Maryland at College Park, USA"}]},{"given":"James","family":"Parker","sequence":"additional","affiliation":[{"name":"University of Maryland at College Park, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5702-0860","authenticated-orcid":false,"given":"Patrick","family":"Redmond","sequence":"additional","affiliation":[{"name":"University of California at Santa Cruz, USA"}]},{"given":"Lindsey","family":"Kuper","sequence":"additional","affiliation":[{"name":"University of California at Santa Cruz, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2759-9223","authenticated-orcid":false,"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"University of Maryland at College Park, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0732-5476","authenticated-orcid":false,"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034691.2034717"},{"key":"e_1_2_2_2_1","volume-title":"Proving Type Class Laws for Haskell. In International Symposium on Trends in Functional Programming. Springer, 61-74","author":"Arvidsson Andreas","year":"2016","unstructured":"Andreas Arvidsson , Moa Johansson , and Robin Touche . 2016 . Proving Type Class Laws for Haskell. In International Symposium on Trends in Functional Programming. Springer, 61-74 . Andreas Arvidsson, Moa Johansson, and Robin Touche. 2016. Proving Type Class Laws for Haskell. In International Symposium on Trends in Functional Programming. Springer, 61-74."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933057.2933090"},{"key":"e_1_2_2_4_1","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet","author":"Barnett Mike","unstructured":"Mike Barnett , K. Rustan M. Leino , and Wolfram Schulte . 2005. The Spec# Programming System: An Overview . In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet , and Traian Muntean (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 49-69. Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. 2005. The Spec# Programming System: An Overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 49-69."},{"key":"e_1_2_2_5_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","volume":"13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , Cesare Tinelli , 2010 . The smt-lib standard: Version 2.0 . In Proceedings of the 8th international workshop on satisfiability modulo theories ( Edinburgh, England) , Vol. 13 . 14. Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England), Vol. 13. 14."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/128738.128742"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341695"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Koen Claessen and John Hughes. 2011. QuickCheck: a lightweight tool for random testing of Haskell programs. Acm sigplan notices 46 4 ( 2011 ) 53-64.  Koen Claessen and John Hughes. 2011. QuickCheck: a lightweight tool for random testing of Haskell programs. Acm sigplan notices 46 4 ( 2011 ) 53-64.","DOI":"10.1145\/1988042.1988046"},{"key":"e_1_2_2_10_1","unstructured":"Koen Claessen Moa Johansson Dan Ros\u00e9n and Nicholas Smallbone. 2012. HipSpec: Automating Inductive Proofs of Program Properties.. In ATx\/WInG at IJCAR. 16-25.  Koen Claessen Moa Johansson Dan Ros\u00e9n and Nicholas Smallbone. 2012. HipSpec: Automating Inductive Proofs of Program Properties.. In ATx\/WInG at IJCAR. 16-25."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Dominique Devriese and Frank Piessens. 2011. On the bright side of type classes: instance arguments in Agda. ACM SIGPLAN Notices 46 9 ( 2011 ) 143-155.  Dominique Devriese and Frank Piessens. 2011. On the bright side of type classes: instance arguments in Agda. ACM SIGPLAN Notices 46 9 ( 2011 ) 143-155.","DOI":"10.1145\/2034574.2034796"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190215.1190229"},{"key":"e_1_2_2_16_1","unstructured":"Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. CoRR abs\/1610.07978 ( 2016 ). arXiv: 1610.07978 http:\/\/arxiv.org\/abs\/1610.07978  Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. CoRR abs\/1610.07978 ( 2016 ). arXiv: 1610.07978 http:\/\/arxiv.org\/abs\/1610.07978"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430532.2364522"},{"key":"e_1_2_2_18_1","volume-title":"Functional Reactive Animation. In International Conference on Functional Programming. http:\/\/conal.net\/papers\/icfp97\/","author":"Elliott Conal","year":"1997","unstructured":"Conal Elliott and Paul Hudak . 1997 . Functional Reactive Animation. In International Conference on Functional Programming. http:\/\/conal.net\/papers\/icfp97\/ Conal Elliott and Paul Hudak. 1997. Functional Reactive Animation. In International Conference on Functional Programming. http:\/\/conal.net\/papers\/icfp97\/"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804303"},{"key":"e_1_2_2_20_1","first-page":"56","volume-title":"Proceedings of the 11th Australian Computer Science Conference 10","author":"Fidge C. J.","year":"1988","unstructured":"C. J. Fidge . 1988 . Timestamps in message-passing systems that preserve the partial ordering . Proceedings of the 11th Australian Computer Science Conference 10 , 1 ( 1988 ), 56 - 66 . http:\/\/sky.scitech.qut.edu.au\/~fidgec\/Publications\/fidge88a.pdf C. J. Fidge. 1988. Timestamps in message-passing systems that preserve the partial ordering. Proceedings of the 11th Australian Computer Science Conference 10, 1 ( 1988 ), 56-66. http:\/\/sky.scitech.qut.edu.au\/~fidgec\/Publications\/fidge88a.pdf"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804303"},{"key":"e_1_2_2_22_1","unstructured":"GHC 2020. GHC: The Glasgow Haskell compiler. https:\/\/www.haskell.org\/ghc\/.  GHC 2020. GHC: The Glasgow Haskell compiler. https:\/\/www.haskell.org\/ghc\/."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133933"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342591"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Marc Shapiro Nuno Pregui\u00e7a Carlos Baquero and Marek Zawirski. 2011a. A comprehensive study of convergent and commutative replicated data types. ( 2011 ).  Marc Shapiro Nuno Pregui\u00e7a Carlos Baquero and Marek Zawirski. 2011a. A comprehensive study of convergent and commutative replicated data types. ( 2011 ).","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_2_27_1","volume-title":"Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago","author":"Shapiro Marc","unstructured":"Marc Shapiro , Nuno Pregui\u00e7a , Carlos Baquero , and Marek Zawirski . 2011b. Conflict-Free Replicated Data Types . In Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago , Franck Petit, and Vincent Villain (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 386-400. Marc Shapiro, Nuno Pregui\u00e7a, Carlos Baquero, and Marek Zawirski. 2011b. Conflict-Free Replicated Data Types. In Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago, Franck Petit, and Vincent Villain (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 386-400."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_2_2_30_1","volume-title":"Zeno: An Automated Prover for Properties of Recursive Data Structures. In Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanagan and Barbara K\u00f6nig (Eds.)","author":"Sonnex William","year":"2012","unstructured":"William Sonnex , Sophia Drossopoulou , and Susan Eisenbach . 2012 . Zeno: An Automated Prover for Properties of Recursive Data Structures. In Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanagan and Barbara K\u00f6nig (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 407-421. William Sonnex, Sophia Drossopoulou, and Susan Eisenbach. 2012. Zeno: An Automated Prover for Properties of Recursive Data Structures. In Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanagan and Barbara K\u00f6nig (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 407-421."},{"key":"e_1_2_2_31_1","volume-title":"Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.)","author":"Sozeau Matthieu","unstructured":"Matthieu Sozeau and Nicolas Oury . 2008. First-Class Type Classes . In Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg , 278-293. Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 278-293."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_2_2_33_1","unstructured":"Bjarne Stroustrup. 1989. Multiple inheritance for C++. Computing Systems 2 4 ( 1989 ) 367-395.  Bjarne Stroustrup. 1989. Multiple inheritance for C++. Computing Systems 2 4 ( 1989 ) 367-395."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_2_35_1","unstructured":"Dotty Development Team. 2020. Dotty Documentation. https:\/\/dotty.epfl.ch\/docs\/reference\/contextual\/type-classes.html  Dotty Development Team. 2020. Dotty Documentation. https:\/\/dotty.epfl.ch\/docs\/reference\/contextual\/type-classes.html"},{"key":"e_1_2_2_36_1","unstructured":"Team Mozilla Research. 2017. The Rust Programming Language. https:\/\/www.rust-lang.org\/en-US\/  Team Mozilla Research. 2017. The Rust Programming Language. https:\/\/www.rust-lang.org\/en-US\/"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242756"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Dimitrios Vytiniotis Simon L. Peyton Jones Koen Claessen and Dan Ros\u00e9n. 2013. HALO: haskell to logic through denotational semantics. In POPL.  Dimitrios Vytiniotis Simon L. Peyton Jones Koen Claessen and Dan Ros\u00e9n. 2013. HALO: haskell to logic through denotational semantics. In POPL.","DOI":"10.1145\/2429069.2429121"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341705"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2009.75"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371121"},{"key":"e_1_2_2_46_1","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.)","author":"Zeller Peter","unstructured":"Peter Zeller , Annette Bieniusa , and Arnd Poetzsch-Hefter . 2014. Formal Specification and Verification of CRDTs . In Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg , 33-48. Peter Zeller, Annette Bieniusa, and Arnd Poetzsch-Hefter. 2014. Formal Specification and Verification of CRDTs. In Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 33-48."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428284","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428284","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428284","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:58Z","timestamp":1750197778000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428284"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":45,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428284"],"URL":"https:\/\/doi.org\/10.1145\/3428284","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}