{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:15Z","timestamp":1750220835734,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T00:00:00Z","timestamp":1565222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1453508"],"award-info":[{"award-number":["1453508"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,8,8]]},"DOI":"10.1145\/3331545.3342591","type":"proceedings-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:51:45Z","timestamp":1564433505000},"page":"15-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Generic and flexible defaults for verified, law-abiding type-class instances"],"prefix":"10.1145","author":[{"given":"Ryan G.","family":"Scott","sequence":"first","affiliation":[{"name":"Indiana University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryan R.","family":"Newton","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,8,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088355"},{"volume-title":"The Practical Guide to Levitation. Master\u2019s thesis","author":"Al-Sibahi Ahmad Salim","key":"e_1_3_2_2_2_1","unstructured":"Ahmad Salim Al-Sibahi . 2014. The Practical Guide to Levitation. Master\u2019s thesis . IT University of Copenhagen , Copenhagen, Denmark . http:\/\/itu.dk\/people\/asal\/pubs\/msc-thesis-report.pdf Ahmad Salim Al-Sibahi. 2014. The Practical Guide to Levitation. Master\u2019s thesis. IT University of Copenhagen, Copenhagen, Denmark. http:\/\/itu.dk\/people\/asal\/pubs\/msc-thesis-report.pdf"},{"key":"e_1_3_2_2_3_1","unstructured":"Ahmad Salim Al-Sibahi. 2019. Desc\u2019n crunch. https:\/\/github.com\/ahmadsalim\/desc-n-crunch\/tree\/ 6da2675bb4e2f5386c9f6a264ffd64846d11baa9 . Accessed: 2019-01-23.  Ahmad Salim Al-Sibahi. 2019. Desc\u2019n crunch. https:\/\/github.com\/ahmadsalim\/desc-n-crunch\/tree\/ 6da2675bb4e2f5386c9f6a264ffd64846d11baa9 . Accessed: 2019-01-23."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76786-2_4"},{"key":"e_1_3_2_2_5_1","unstructured":"Jeremy Avigad Leonardo de Moura and Soonho Kong. 2017. Type Classes. https:\/\/leanprover.github.io\/theorem_proving_in_lean\/type_ classes.html . Accessed: 2019-01-23.  Jeremy Avigad Leonardo de Moura and Soonho Kong. 2017. Type Classes. https:\/\/leanprover.github.io\/theorem_proving_in_lean\/type_ classes.html . Accessed: 2019-01-23."},{"key":"e_1_3_2_2_6_1","first-page":"4","article-title":"Universes for Generic Programs and Proofs in Dependent Type Theory","volume":"10","author":"Benke Marcin","year":"2003","unstructured":"Marcin Benke , Peter Dybjer , and Patrik Jansson . 2003 . Universes for Generic Programs and Proofs in Dependent Type Theory . Nordic J. of Computing 10 , 4 (Dec. 2003), 265\u2013289. http:\/\/dl.acm.org\/citation.cfm? id=985799.985801 Marcin Benke, Peter Dybjer, and Patrik Jansson. 2003. Universes for Generic Programs and Proofs in Dependent Type Theory. Nordic J. of Computing 10, 4 (Dec. 2003), 265\u2013289. http:\/\/dl.acm.org\/citation.cfm? id=985799.985801","journal-title":"Nordic J. of Computing"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236784"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633634"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_3_2_2_12_1","unstructured":"Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. arXiv: cs.PL\/1610.07978  Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. arXiv: cs.PL\/1610.07978"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364522"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1789277.1789288"},{"key":"e_1_3_2_2_15_1","volume-title":"High Confidence Software and Systems Conference, HCSS04","author":"Hallgren Thomas","year":"2004","unstructured":"Thomas Hallgren , James Hook , Mark P Jones , and Richard B Kieburtz . 2004 . An overview of the programatica toolset . In High Confidence Software and Systems Conference, HCSS04 , http:\/\/www. cse. ogi. edu\/\u02dc hallgren\/Programatica\/HCSS04. Citeseer. Thomas Hallgren, James Hook, Mark P Jones, and Richard B Kieburtz. 2004. An overview of the programatica toolset. In High Confidence Software and Systems Conference, HCSS04, http:\/\/www. cse. ogi. edu\/\u02dc hallgren\/Programatica\/HCSS04. Citeseer."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Pedro Magalh\u00e3es. 2013. Optimisation of Generic Programs Through Inlining. 104\u2013121.  Jos\u00e9 Pedro Magalh\u00e3es. 2013. Optimisation of Generic Programs Through Inlining. 104\u2013121.","DOI":"10.1007\/978-3-642-41582-1_7"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863523.1863529"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706356.1706366"},{"key":"e_1_3_2_2_19_1","unstructured":"Guido Mart\u00ednez. 2018. Typeclasses (via meta arguments). https:\/\/github.com\/FStarLang\/FStar\/wiki\/Typeclasses-(via-metaarguments)\/c5719ae49bc8a00fa231057a94a8edee1db2a704 . Accessed: 2019-01-23.  Guido Mart\u00ednez. 2018. Typeclasses (via meta arguments). https:\/\/github.com\/FStarLang\/FStar\/wiki\/Typeclasses-(via-metaarguments)\/c5719ae49bc8a00fa231057a94a8edee1db2a704 . Accessed: 2019-01-23."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411318.1411321"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342591"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242745"},{"key":"e_1_3_2_2_23_1","volume-title":"Classes of Arbitrary Kind. In International Symposium on Practical Aspects of Declarative Languages. Springer, 150\u2013168","author":"Serrano Alejandro","year":"2019","unstructured":"Alejandro Serrano and Victor Cacciari Miraldo . 2019 . Classes of Arbitrary Kind. In International Symposium on Practical Aspects of Declarative Languages. Springer, 150\u2013168 . Alejandro Serrano and Victor Cacciari Miraldo. 2019. Classes of Arbitrary Kind. In International Symposium on Practical Aspects of Declarative Languages. Springer, 150\u2013168."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236787"},{"key":"e_1_3_2_2_29_1","first-page":"1","article-title":"Proof support for general type classes","volume":"5","author":"Kesteren Ron Van","year":"2006","unstructured":"Ron Van Kesteren , Marko Van Eekelen , and Maarten De Mol . 2006 . Proof support for general type classes . Trends in Functional Programming 5 (2006), 1 \u2013 16 . Ron Van Kesteren, Marko Van Eekelen, and Maarten De Mol. 2006. Proof support for general type classes. Trends in Functional Programming 5 (2006), 1\u201316.","journal-title":"Trends in Functional Programming"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628161"},{"key":"e_1_3_2_2_31_1","volume-title":"Extended Version: Refinement Reflection: Complete Verification with SMT. https:\/\/nikivazou.github.io\/static\/popl18\/extended-refinementreflection.pdf","author":"Vazou Niki","year":"2017","unstructured":"Niki Vazou , Anish Tondwalkar , Vikraman Choudhury , Ryan G. Scott , Ryan R. Newton , Philip Wadler , and Ranjit Jhala . 2017 . Extended Version: Refinement Reflection: Complete Verification with SMT. https:\/\/nikivazou.github.io\/static\/popl18\/extended-refinementreflection.pdf Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2017. Extended Version: Refinement Reflection: Complete Verification with SMT. https:\/\/nikivazou.github.io\/static\/popl18\/extended-refinementreflection.pdf"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_2_2_33_1","volume-title":"Leibniz International Proceedings in Informatics, LIPIcs 21 (01","author":"Vytiniotis Dimitrios","year":"2013","unstructured":"Dimitrios Vytiniotis and Simon Peyton Jones . 2013 . Evidence normalization in system FC . Leibniz International Proceedings in Informatics, LIPIcs 21 (01 2013), 20\u201338. Dimitrios Vytiniotis and Simon Peyton Jones. 2013. Evidence normalization in system FC. Leibniz International Proceedings in Informatics, LIPIcs 21 (01 2013), 20\u201338."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596585"}],"event":{"name":"ICFP '19: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Berlin Germany","acronym":"ICFP '19"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331545.3342591","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331545.3342591","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331545.3342591","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:39Z","timestamp":1750202019000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331545.3342591"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,8]]},"references-count":36,"alternative-id":["10.1145\/3331545.3342591","10.1145\/3331545"],"URL":"https:\/\/doi.org\/10.1145\/3331545.3342591","relation":{},"subject":[],"published":{"date-parts":[[2019,8,8]]},"assertion":[{"value":"2019-08-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}