{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:25Z","timestamp":1767929545115,"version":"3.49.0"},"reference-count":34,"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\/"}],"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            Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting\n            <jats:italic toggle=\"yes\">Quotient Haskell<\/jats:italic>\n            , an extension of Liquid Haskell with support for quotient types.\n          <\/jats:p>","DOI":"10.1145\/3632869","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"785-815","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Quotient Haskell: Lightweight Quotient Types for All"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-8731-6963","authenticated-orcid":false,"given":"Brandon","family":"Hewer","sequence":"first","affiliation":[{"name":"University of Nottingham, Nottingham, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9584-5150","authenticated-orcid":false,"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"University of Nottingham, Nottingham, UK"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"crossref","unstructured":"Michael Abbott Thorsten Altenkirch Neil Ghani and Conor McBride. 2004. Constructing Polymorphic Programs with Quotient Types. In Proceedings of the International Conference on Mathematics of Program Construction.","DOI":"10.1007\/978-3-540-27764-4_2"},{"key":"e_1_3_1_3_1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch Paolo Capriotti Gabe Dijkstra Nicolai Kraus and Fredrik Nordvall Forsberg. 2018. Quotient Inductive-Inductive Types. In Proceedings of the Conference on Foundations of Software Science and Computation Structures.","DOI":"10.1007\/978-3-319-89366-2_16"},{"key":"e_1_3_1_4_1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch and Ambrus Kaposi. 2016. Type Theory in Type Theory Using Quotient Inductive Types. In Proceedings of the Symposium on Principles of Programming Languages.","DOI":"10.1145\/2837614.2837638"},{"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.1017\/S0960129517000184"},{"key":"e_1_3_1_7_1","doi-asserted-by":"crossref","unstructured":"Cyril Cohen. 2013. Pragmatic Quotient Types in Coq. In Proceedings of the International Conference on Interactive Theorem Proving.","DOI":"10.1007\/978-3-642-39634-2_17"},{"key":"e_1_3_1_8_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development\u00a0System","author":"Constable R. L.","year":"1986","unstructured":"R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development\u00a0System. Prentice-Hall, Inc., USA."},{"key":"e_1_3_1_9_1","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura Soonho Kong Jeremy Avigad Floris Van Doorn and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Proceedings of the International Conference on Automated Deduction.","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_1_10_1","doi-asserted-by":"crossref","unstructured":"Tim Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proceedings of the Conference on Programming Language Design and Implementation.","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_1_11_1","unstructured":"Zachary Grannan Niki Vazou Eva Darulova and Alexander J Summers. 2022. REST: Integrating Term Rewriting with Program Verification (Extended Version). (2022). arXiv preprint arXiv:2202.05872."},{"key":"e_1_3_1_12_1","unstructured":"Brandon Hewer. 2023. Quotient Haskell. https:\/\/github.com\/brandonhewer\/QuotientHaskell\/tree\/develop."},{"key":"e_1_3_1_13_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. 1995. A Simple Model for Quotient Types. In Proceedings of the International Conference on Typed Lambda Calculi and Applications.","DOI":"10.1007\/BFb0014055"},{"key":"e_1_3_1_14_1","doi-asserted-by":"crossref","unstructured":"Brian Huffman and Ondrej Kuncar. 2013. Lifting and Transfer: A Modular Design for Quotients in Isabelle\/HOL. In Proceedings of the International Certified Programs and Proofs.","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","unstructured":"Cezary Kaliszyk and Christian Urban. 2011. Quotients Revisited for Isabelle\/HOL. In Proceedings of the Symposium on Applied Computing.","DOI":"10.1145\/1982185.1982529"},{"key":"e_1_3_1_16_1","doi-asserted-by":"crossref","unstructured":"Ambrus Kaposi Andr\u00e1s Kov\u00e1cs and Thorsten Altenkirch. 2019. Constructing Quotient Inductive-Inductive Types. Proceedings of the ACM on Programming Languages 3 POPL (2019).","DOI":"10.1145\/3290315"},{"key":"e_1_3_1_17_1","doi-asserted-by":"crossref","unstructured":"Ming Kawaguchi Patrick M Rondon and Ranjit Jhala. 2010. Dsolve: Safety Verification via Liquid Types. In Proceedings of the International Conference on Computer Aided Verification.","DOI":"10.1007\/978-3-642-14295-6_12"},{"key":"e_1_3_1_18_1","doi-asserted-by":"crossref","unstructured":"Jan Willem Klop Vincent van Oostrom and Roel de Vrijer. 2008. Lambda Calculus with Patterns. Theoretical Computer Science 398 (2008).","DOI":"10.1016\/j.tcs.2008.01.019"},{"key":"e_1_3_1_19_1","volume-title":"Quotient Types in Type Theory","author":"Li Nuo","year":"2015","unstructured":"Nuo Li. 2015. Quotient Types in Type Theory. Ph.D. Dissertation. University of Nottingham."},{"key":"e_1_3_1_20_1","unstructured":"Lambert Meertens. 1983. Algorithmics: Towards Programming as a Mathematical Activity. In Proceedings of the CWI Symposium on Mathematics and Computer Science."},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_18"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183280"},{"key":"e_1_3_1_23_1","doi-asserted-by":"crossref","unstructured":"Patrick M Rondon Ming Kawaguci and Ranjit Jhala. 2008. Liquid Types. In Proceedings of Conference on Programming Language Design and Implementation.","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_3_1_25_1","doi-asserted-by":"crossref","unstructured":"Oscar Slotosch. 1997. Higher Order Quotients and their Implementation in Isabelle HOL. In Proceedings of the International Conference on Theorem Proving in Higher Order Logics.","DOI":"10.1007\/BFb0028401"},{"key":"e_1_3_1_26_1","doi-asserted-by":"crossref","unstructured":"Simon Thompson. 1986. Laws in Miranda. In Proceedings of the ACM Conference on LISP and Functional Programming.","DOI":"10.1145\/319838.319839"},{"key":"e_1_3_1_27_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"The Univalent Foundations Program","year":"2013","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study."},{"key":"e_1_3_1_28_1","doi-asserted-by":"crossref","unstructured":"Floris van Doorn Jakob von Raumer and Ulrik Buchholtz. 2017. Homotopy Type Theory in Lean. In Proceedings of the International Conference on Interactive Theorem Proving.","DOI":"10.1007\/978-3-319-66107-0_30"},{"key":"e_1_3_1_29_1","unstructured":"Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph.D. Dissertation. University of California San Diego."},{"key":"e_1_3_1_30_1","doi-asserted-by":"crossref","unstructured":"Niki Vazou Alexander Bakst and Ranjit Jhala. 2015. Bounded Refinement Types. In Proceedings of the International Conference on Functional Programming.","DOI":"10.1145\/2784731.2784745"},{"key":"e_1_3_1_31_1","doi-asserted-by":"crossref","unstructured":"Niki Vazou and Michael Greenberg. 2022. How to Safely Use Extensionality in Liquid Haskell. In Proceedings of the 15th ACM SIGPLAN International Haskell Symposium. 13\u201326.","DOI":"10.1145\/3546189.3549919"},{"key":"e_1_3_1_32_1","doi-asserted-by":"crossref","unstructured":"Niki Vazou Patrick M Rondon and Ranjit Jhala. 2013. Abstract Refinement Types. In Proceedings of the European Symposium on Programming.","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_3_1_33_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 Proceedings of the International Conference on Functional Programming.","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_34_1","article-title":"Refinement Reflection: Complete Verification with SMT","volume":"2","author":"Vazou Niki","year":"2017","unstructured":"Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G Scott, Ryan R Newton, Philip Wadler, and Ranjit Jhala. 2017. Refinement Reflection: Complete Verification with SMT. Proceedings of the ACM on Programming Languages 2, POPL (2017).","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_1_35_1","doi-asserted-by":"crossref","unstructured":"Andrea Vezzosi Anders M\u00f6rtberg and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proceedings of the ACM on Programming Languages 3 ICFP (2019).","DOI":"10.1145\/3341691"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632869","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632869","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:02:12Z","timestamp":1751659332000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632869"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":34,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632869"],"URL":"https:\/\/doi.org\/10.1145\/3632869","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"}}]}}