{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:33:06Z","timestamp":1767339186714,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,28]],"date-time":"2013-09-28T00:00:00Z","timestamp":1380326400000},"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":[[2013,9,28]]},"DOI":"10.1145\/2502488.2502495","type":"proceedings-article","created":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T19:57:05Z","timestamp":1379447825000},"page":"25-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Dependent type providers"],"prefix":"10.1145","author":[{"given":"David Raymond","family":"Christiansen","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,9,28]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/647100.717294"},{"volume-title":"Chalmers University of Technology","year":"2011","author":"Andjelkovic S.","key":"e_1_3_2_1_2_1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/985799.985801"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1376616.1376746"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"volume-title":"University of Durham","year":"2005","author":"Brady E.","key":"e_1_3_2_1_6_1"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929536"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"E.\n       \n      Brady C.\n       \n      McBride and \n      \n      \n      J.\n       \n      McKinna\n    .\n      \n  \n   \n  Inductive families need not store their indices. In S. Berardi M. Coppo and F. Damiani editors Types for Proofs and Programs volume \n  3085\n   of \n  Lecture Notes in Computer Science pages \n  115\n  --\n  129\n  . \n  Springer Berlin Heidelberg 2004\n  .  E. Brady C. McBride and J. McKinna. Inductive families need not store their indices. In S. Berardi M. Coppo and F. Damiani editors Types for Proofs and Programs volume 3085 of Lecture Notes in Computer Science pages 115--129. Springer Berlin Heidelberg 2004.","DOI":"10.1007\/978-3-540-24849-1_8"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806612"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325709"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01806312"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"L.\n       \n      Moura\n     and \n      \n      \n      N.\n       \n      Bj\u00f8rner\n      \n  \n  . \n  Z3: An efficient SMT solver. In C. Ramakrishnan and J. Rehof editors phTools and Algorithms for the Construction and Analysis of Systems volume \n  4963\n   of \n  Lecture Notes in Computer Science pages \n  337\n  --\n  340\n  . \n  Springer Berlin Heidelberg 2008\n  .   L. Moura and N. Bj\u00f8rner. Z3: An efficient SMT solver. In C. Ramakrishnan and J. Rehof editors phTools and Algorithms for the Construction and Analysis of Systems volume 4963 of Lecture Notes in Computer Science pages 337--340. Springer Berlin Heidelberg 2008.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411203.1411213"},{"key":"e_1_3_2_1_17_1","unstructured":"The Agda team. The Agda wiki 2013. http:\/\/wiki.portal.chalmers.se\/agda\/.  The Agda team. The Agda wiki 2013. http:\/\/wiki.portal.chalmers.se\/agda\/."},{"volume-title":"LogiCal Project","year":"2004","key":"e_1_3_2_1_18_1"},{"key":"e_1_3_2_1_19_1","unstructured":"P. van der Walt. Reflection in Agda 2012. M.Sc. Thesis. Available online at http:\/\/igitur-archive.library.uu.nl\/student-theses\/2012-1030-200720\/UUindex.html.  P. van der Walt. Reflection in Agda 2012. M.Sc. Thesis. Available online at http:\/\/igitur-archive.library.uu.nl\/student-theses\/2012-1030-200720\/UUindex.html."}],"event":{"name":"ICFP'13: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston Massachusetts USA","acronym":"ICFP'13"},"container-title":["Proceedings of the 9th ACM SIGPLAN workshop on Generic programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502488.2502495","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2502488.2502495","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:36Z","timestamp":1750231716000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502488.2502495"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,28]]},"references-count":18,"alternative-id":["10.1145\/2502488.2502495","10.1145\/2502488"],"URL":"https:\/\/doi.org\/10.1145\/2502488.2502495","relation":{},"subject":[],"published":{"date-parts":[[2013,9,28]]},"assertion":[{"value":"2013-09-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}