{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:21Z","timestamp":1772164101931,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,9,17]],"date-time":"2018-09-17T00:00:00Z","timestamp":1537142400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,9,17]]},"DOI":"10.1145\/3242744.3242756","type":"proceedings-article","created":{"date-parts":[[2018,9,18]],"date-time":"2018-09-18T08:11:39Z","timestamp":1537258299000},"page":"132-144","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)"],"prefix":"10.1145","author":[{"given":"Niki","family":"Vazou","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Joachim","family":"Breitner","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"given":"Rose","family":"Kunkel","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"David","family":"Van Horn","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"University of Nottingham, UK"}]}],"member":"320","published-online":{"date-parts":[[2018,9,17]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Calculating correct compilers. Journal of Functional Programming 25","author":"Bahr Patrick","year":"2015","unstructured":"Patrick Bahr and Graham Hutton . 2015. Calculating correct compilers. Journal of Functional Programming 25 ( 2015 ). Patrick Bahr and Graham Hutton. 2015. Calculating correct compilers. Journal of Functional Programming 25 (2015)."},{"key":"e_1_3_2_1_2_1","unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0.  Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0."},{"key":"e_1_3_2_1_3_1","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2004. Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions . Springer . Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Springer."},{"key":"e_1_3_2_1_4_1","volume-title":"An Introduction to the Theory of Lists","author":"Bird Richard S.","unstructured":"Richard S. Bird . 1987. An Introduction to the Theory of Lists . In NATO ASI. Springer , 5\u201342. Richard S. Bird. 1987. An Introduction to the Theory of Lists. In NATO ASI. Springer, 5\u201342."},{"key":"e_1_3_2_1_5_1","volume-title":"Pearls of Functional Algorithm Design","author":"Bird Richard S.","unstructured":"Richard S. Bird . 2010. Pearls of Functional Algorithm Design . Cambridge University Press . Richard S. Bird. 2010. Pearls of Functional Algorithm Design. Cambridge University Press."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242748"},{"key":"e_1_3_2_1_8_1","volume-title":"CADE-25 (LNCS)","author":"de Moura Leonardo Mendon\u00e7a","unstructured":"Leonardo Mendon\u00e7a de Moura , Soonho Kong , Jeremy Avigad , Floris van Doorn , and Jakob von Raumer . 2015. The Lean Theorem Prover (System Description) . In CADE-25 (LNCS) , Vol. 9195 . Springer , 378\u2013388. Leonardo Mendon\u00e7a de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In CADE-25 (LNCS), Vol. 9195. Springer, 378\u2013388."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804303"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706356.1706385"},{"key":"e_1_3_2_1_13_1","volume-title":"Programming in Haskell","author":"Hutton Graham","unstructured":"Graham Hutton . 2016. Programming in Haskell . Cambridge University Press . Graham Hutton. 2016. Programming in Haskell. Cambridge University Press."},{"key":"e_1_3_2_1_14_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR (LNCS)","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR (LNCS) , Vol. 6355 . Springer , 348\u2013370. K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR (LNCS), Vol. 6355. Springer, 348\u2013370."},{"key":"e_1_3_2_1_15_1","volume-title":"Leino and Cl\u00e9ment Pit-Claudel","author":"K. Rustan","year":"2016","unstructured":"K. Rustan M. Leino and Cl\u00e9ment Pit-Claudel . 2016 . Trigger Selection Strategies to Stabilize Program Verifiers. In CAV (LNCS), Vol. 9779 . Springer , 361\u2013381. K. Rustan M. Leino and Cl\u00e9ment Pit-Claudel. 2016. Trigger Selection Strategies to Stabilize Program Verifiers. In CAV (LNCS), Vol. 9779. Springer, 361\u2013381."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_9"},{"key":"e_1_3_2_1_17_1","volume-title":"Functional Pearl: A type-correct, stack-safe, provably correct expression compiler in Epigram.","author":"Mckinna James","year":"2006","unstructured":"James Mckinna and Joel Wright . 2006 . Functional Pearl: A type-correct, stack-safe, provably correct expression compiler in Epigram. (2006). James Mckinna and Joel Wright. 2006. Functional Pearl: A type-correct, stack-safe, provably correct expression compiler in Epigram. (2006)."},{"key":"e_1_3_2_1_18_1","volume-title":"Types for Proofs and Programs (TYPES) (LNCS)","author":"Nipkow Tobias","unstructured":"Tobias Nipkow . 2002. Structured Proofs in Isar\/HOL . In Types for Proofs and Programs (TYPES) (LNCS) , Vol. 2646 . Springer . Tobias Nipkow. 2002. Structured Proofs in Isar\/HOL. In Types for Proofs and Programs (TYPES) (LNCS), Vol. 2646. Springer."},{"key":"e_1_3_2_1_19_1","volume-title":"LNCS","volume":"2283","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2002 . Isabelle\/HOL - A Proof Assistant for Higher-Order Logic . LNCS , Vol. 2283 . Springer. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, Vol. 2283. Springer."},{"key":"e_1_3_2_1_21_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u02c7at\u02c7alin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2018","unstructured":"Benjamin C. Pierce , Arthur Azevedo de Amorim , Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u02c7at\u02c7alin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey. 2018 . Software Foundations Volume 1: Logical Foundations. Electronic textbook. Version 5.5. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf . Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u02c7at\u02c7alin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey. 2018. Software Foundations Volume 1: Logical Foundations. Electronic textbook. Version 5.5. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf ."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_25_1","unstructured":"Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph.D. Dissertation. University of California San Diego.  Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph.D. Dissertation. University of California San Diego."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122963"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"}],"event":{"name":"ICFP '18: 23nd ACM SIGPLAN International Conference on Functional Programming","location":"St. Louis MO USA","acronym":"ICFP '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3242744.3242756","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3242744.3242756","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:57:22Z","timestamp":1750193842000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3242744.3242756"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,17]]},"references-count":27,"alternative-id":["10.1145\/3242744.3242756","10.1145\/3242744"],"URL":"https:\/\/doi.org\/10.1145\/3242744.3242756","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3299711.3242756","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,9,17]]},"assertion":[{"value":"2018-09-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}