{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:56Z","timestamp":1772164076174,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,8,30]],"date-time":"2015-08-30T00:00:00Z","timestamp":1440892800000},"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":[[2015,8,30]]},"DOI":"10.1145\/2804302.2804307","type":"proceedings-article","created":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T10:09:20Z","timestamp":1440410960000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Improving Haskell types with SMT"],"prefix":"10.1145","author":[{"given":"Iavor S.","family":"Diatchki","sequence":"first","affiliation":[{"name":"Galois, USA"}]}],"member":"320","published-online":{"date-parts":[[2015,8,30]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Yices Manual 2015. URL http:\/\/yices.csl.sri.com\/papers\/ manual.pdf.  Yices Manual 2015. URL http:\/\/yices.csl.sri.com\/papers\/ manual.pdf."},{"key":"e_1_3_2_1_2_1","volume-title":"A typechecker plugin for units of measure. Submitted for publication","author":"Gundry Adam","year":"2015","unstructured":"Adam Gundry . A typechecker plugin for units of measure. Submitted for publication ., 2015 . Adam Gundry. A typechecker plugin for units of measure. Submitted for publication., 2015."},{"key":"e_1_3_2_1_3_1","volume-title":"A plug-in for normalising type literals in ghc","author":"Baaij Christiaan","year":"2015","unstructured":"Christiaan Baaij . A plug-in for normalising type literals in ghc . 2015 . URL https:\/\/github.com\/clash-lang\/ ghc-typelits-natnormalise. Christiaan Baaij. A plug-in for normalising type literals in ghc. 2015. URL https:\/\/github.com\/clash-lang\/ ghc-typelits-natnormalise."},{"key":"e_1_3_2_1_4_1","volume-title":"Department of Computer Science","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . The SMT-LIB standard: Version 2.0. Technical report , Department of Computer Science , The University of Iowa , 2010 . URL http:\/\/smtlib.cs. uiowa.edu\/papers\/smt-lib-reference-v2.0-r12.09.09.pdf. Clark Barrett, Aaron Stump, and Cesare Tinelli. The SMT-LIB standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa, 2010. URL http:\/\/smtlib.cs. uiowa.edu\/papers\/smt-lib-reference-v2.0-r12.09.09.pdf."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification","author":"Barrett Clark","year":"2011","unstructured":"Clark Barrett , Christopher L. Conway , Morgan Deters , Liana Hadarean , Dejan Jovanovi\u00b4c , Tim King , Andrew Reynolds , and Cesare Tinelli . CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification , Snowbird, Utah, USA , 2011 . URL http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032319. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u00b4c, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification, Snowbird, Utah, USA, 2011. URL http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032319."},{"key":"e_1_3_2_1_6_1","volume-title":"24th International Conference on Rewriting Techniques and Applications","author":"Vytiniotis Dimitrios","year":"2013","unstructured":"Dimitrios Vytiniotis and Simon Peyton Jones . Evidence normalization in System FC . In 24th International Conference on Rewriting Techniques and Applications , Eindhoven, Netherlands , 2013 . URL http:\/\/research.microsoft.com\/en-us\/um\/people\/simonpj\/ papers\/ext-f\/fc-new-tyco.pdf. Dimitrios Vytiniotis and Simon Peyton Jones. Evidence normalization in System FC. In 24th International Conference on Rewriting Techniques and Applications, Eindhoven, Netherlands, 2013. URL http:\/\/research.microsoft.com\/en-us\/um\/people\/simonpj\/ papers\/ext-f\/fc-new-tyco.pdf."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_1_9_1","volume-title":"simple-smt: a Haskell library for working with SMT solvers","author":"Diatchki Iavor S.","year":"2015","unstructured":"Iavor S. Diatchki . simple-smt: a Haskell library for working with SMT solvers , 2015 . URL http:\/\/hackage.haskell.org\/package\/ simple-smt. Iavor S. Diatchki. simple-smt: a Haskell library for working with SMT solvers, 2015. URL http:\/\/hackage.haskell.org\/package\/ simple-smt."},{"key":"e_1_3_2_1_10_1","volume-title":"A plug-in for solving linear constraints using an smt solver","author":"Diatchki Iavor S.","year":"2015","unstructured":"Iavor S. Diatchki . A plug-in for solving linear constraints using an smt solver . 2015 . URL https:\/\/github.com\/yav\/type-nat-solver. Iavor S. Diatchki. A plug-in for solving linear constraints using an smt solver. 2015. URL https:\/\/github.com\/yav\/type-nat-solver."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863596"},{"key":"e_1_3_2_1_12_1","volume-title":"14th International Conference","author":"de Moura Leonardo","year":"2008","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . Z3 : An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems , 14th International Conference , Budapest, Hungary , 2008 . URL http:\/\/research.microsoft.com\/projects\/z3\/z3.pdf. Leonardo de Moura and Nikolaj Bj\u00f8rner. Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, Budapest, Hungary, 2008. URL http:\/\/research.microsoft.com\/projects\/z3\/z3.pdf."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224198"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628146"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633361"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364522"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503786"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765921"},{"key":"e_1_3_2_1_20_1","volume-title":"Version 7.10.1","author":"Team The GHC","year":"2015","unstructured":"The GHC Team . The Glorious Glasgow Haskell Compilation System User\u2019s Guide , Version 7.10.1 , 2015 . URL https:\/\/downloads. haskell.org\/~ghc\/7.10.1\/docs\/html\/users_guide\/index. html. The GHC Team. The Glorious Glasgow Haskell Compilation System User\u2019s Guide, Version 7.10.1, 2015. URL https:\/\/downloads. haskell.org\/~ghc\/7.10.1\/docs\/html\/users_guide\/index. html."}],"event":{"name":"ICFP'15: 20th ACM SIGPLAN International Conference on Functional Programming","location":"Vancouver BC Canada","acronym":"ICFP'15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2804302.2804307","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2804302.2804307","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:07:09Z","timestamp":1750208829000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2804302.2804307"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,30]]},"references-count":20,"alternative-id":["10.1145\/2804302.2804307","10.1145\/2804302"],"URL":"https:\/\/doi.org\/10.1145\/2804302.2804307","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2887747.2804307","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,8,30]]},"assertion":[{"value":"2015-08-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}