{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:23Z","timestamp":1775873663676,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,6]],"date-time":"2022-09-06T00:00:00Z","timestamp":1662422400000},"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":[[2022,9,6]]},"DOI":"10.1145\/3546189.3549921","type":"proceedings-article","created":{"date-parts":[[2022,9,6]],"date-time":"2022-09-06T20:24:01Z","timestamp":1662495841000},"page":"27-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Liquid proof macros"],"prefix":"10.1145","author":[{"given":"Henry","family":"Blanchette","sequence":"first","affiliation":[{"name":"University of Maryland at College Park, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonidas","family":"Lampropoulos","sequence":"additional","affiliation":[{"name":"University of Maryland at College Park, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,9,6]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"CVC4","author":"Barrett Clark","unstructured":"Clark Barrett , Christopher L. Conway , Morgan Deters , Liana Hadarean , Dejan Jovanovi\u0107 , Tim King , Andrew Reynolds , and Cesare Tinelli . 2011. CVC4 . In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 171\u2013177. isbn:978-3-642-22110-1 Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u0107, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 171\u2013177. isbn:978-3-642-22110-1"},{"key":"e_1_3_2_1_2_1","volume-title":"The SMT-LIB Standard: Version 2.0. Department of Computer Science","author":"Barrett Clark","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . 2010. The SMT-LIB Standard: Version 2.0. Department of Computer Science , The University of Iowa . Available at www.SMT-LIB.org Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3554302"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9278-5"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000283"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409026"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_3"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_11_1","volume-title":"Frank Pfenning (Ed.) (Electronic Notes in Theoretical Computer Science (ENTCS)","volume":"109","author":"Delahaye David","year":"2002","unstructured":"David Delahaye . 2002 . A Proof Dedicated Meta-Language. In Logical Frameworks and Meta-Languages (LFM) , Frank Pfenning (Ed.) (Electronic Notes in Theoretical Computer Science (ENTCS) , Vol. 70(2)). Elsevier, Copenhagen (Denmark). 96\u2013 109 . David Delahaye. 2002. A Proof Dedicated Meta-Language. In Logical Frameworks and Meta-Languages (LFM), Frank Pfenning (Ed.) (Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 70(2)). Elsevier, Copenhagen (Denmark). 96\u2013109."},{"key":"e_1_3_2_1_12_1","volume-title":"Dependent Types in Haskell: Theory and Practice. Ph. D. Dissertation","author":"Eisenberg Richard A.","unstructured":"Richard A. Eisenberg . 2016. Dependent Types in Haskell: Theory and Practice. Ph. D. Dissertation . University of Pennsylvania . arxiv:1610.07978 Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph. D. Dissertation. University of Pennsylvania. arxiv:1610.07978"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"T. Freeman and F. Pfenning. 1991. Refinement Types for ML. In PLDI. \t\t\t\t\t  T. Freeman and F. Pfenning. 1991. Refinement Types for ML. In PLDI.","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_1_14_1","unstructured":"Mustafa Hafidi. 2020. From testing to formal verification in Haskell. Ph. D. Dissertation. ETSI_Informatica. https:\/\/oa.upm.es\/63616\/ \t\t\t\t\t  Mustafa Hafidi. 2020. From testing to formal verification in Haskell. Ph. D. Dissertation. ETSI_Informatica. https:\/\/oa.upm.es\/63616\/"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_2_1_17_1","volume-title":"Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.)","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Sebastian Ullrich . 2021. The Lean 4 Theorem Prover and Programming Language . In Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.) . Springer International Publishing , Cham . 625\u2013635. isbn:978-3-030-79876-5 Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham. 625\u2013635. isbn:978-3-030-79876-5"},{"key":"e_1_3_2_1_18_1","volume-title":"a proof assistant for higher-order logic. 2283","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : a proof assistant for higher-order logic. 2283 , Springer Science & Business Media . Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. 2283, Springer Science & Business Media."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523707"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.29007\/36dt"},{"key":"e_1_3_2_1_21_1","volume-title":"The Fifth International Workshop on Coq for Programming LanguagesCoqPL. https:\/\/www.p\u00e9drot.fr\/articles\/coqpl2019","author":"P\u00e9drot Pierre-Marie","year":"2019","unstructured":"Pierre-Marie P\u00e9drot . 2019 . Ltac2: Tactical Warfare . The Fifth International Workshop on Coq for Programming LanguagesCoqPL. https:\/\/www.p\u00e9drot.fr\/articles\/coqpl2019 .pdfpdf Pierre-Marie P\u00e9drot. 2019. Ltac2: Tactical Warfare. The Fifth International Workshop on Coq for Programming LanguagesCoqPL. https:\/\/www.p\u00e9drot.fr\/articles\/coqpl2019.pdfpdf"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"N. Swamy C. Hri\u0163cu C. Keller A. Rastogi A. Delignat-Lavaud S. Forest K. Bhargavan C. Fournet P. Strub M. Kohlweiss J. Zinzindohoue and S. Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In POPL. \t\t\t\t\t  N. Swamy C. Hri\u0163cu C. Keller A. Rastogi A. Delignat-Lavaud S. Forest K. Bhargavan C. Fournet P. Strub M. Kohlweiss J. Zinzindohoue and S. Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In POPL.","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3744225"},{"key":"e_1_3_2_1_24_1","volume-title":"Liquid Haskell: Haskell as a theorem prover. Ph. D. Dissertation. UCSD.","author":"Vazou N.","year":"2016","unstructured":"N. Vazou . 2016 . Liquid Haskell: Haskell as a theorem prover. Ph. D. Dissertation. UCSD. N. Vazou. 2016. Liquid Haskell: Haskell as a theorem prover. Ph. D. Dissertation. UCSD."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242756"},{"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\/3158141"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"e_1_3_2_1_29_1","volume-title":"Mtac: A monad for typed tactic programming in Coq. Journal of Functional Programming, 25","author":"Ziliani Beta","year":"2015","unstructured":"Beta Ziliani , Derek Dreyer , Neelakantan R. Krishnaswami , Aleksandar Nanevski , and Viktor Vafeiadis . 2015 . Mtac: A monad for typed tactic programming in Coq. Journal of Functional Programming, 25 (2015). Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis. 2015. Mtac: A monad for typed tactic programming in Coq. Journal of Functional Programming, 25 (2015)."}],"event":{"name":"Haskell '22: 15th ACM SIGPLAN International Haskell Symposium","location":"Ljubljana Slovenia","acronym":"Haskell '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Haskell Symposium"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3546189.3549921","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3546189.3549921","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:23Z","timestamp":1750186823000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3546189.3549921"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,6]]},"references-count":29,"alternative-id":["10.1145\/3546189.3549921","10.1145\/3546189"],"URL":"https:\/\/doi.org\/10.1145\/3546189.3549921","relation":{},"subject":[],"published":{"date-parts":[[2022,9,6]]},"assertion":[{"value":"2022-09-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}