{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:26Z","timestamp":1772164046706,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,9,13]],"date-time":"2012-09-13T00:00:00Z","timestamp":1347494400000},"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":[[2012,9,13]]},"DOI":"10.1145\/2364506.2364522","type":"proceedings-article","created":{"date-parts":[[2012,9,12]],"date-time":"2012-09-12T09:01:27Z","timestamp":1347440487000},"page":"117-130","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["Dependently typed programming with singletons"],"prefix":"10.1145","author":[{"given":"Richard A.","family":"Eisenberg","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,9,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581494"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863592"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017473"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.76.4"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581698"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762221"},{"key":"e_1_3_2_1_12_1","volume-title":"LogiCal Project","author":"Coq","year":"2004","unstructured":"Coq development team. The Coq proof assistant reference manual . LogiCal Project , 2004 . URL http:\/\/coq.inria.fr. Version 8.0. Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. URL http:\/\/coq.inria.fr. Version 8.0."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190229"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890030"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411218"},{"key":"e_1_3_2_1_17_1","volume-title":"9th Symposium on Trends in Functional Programming","author":"Guillemette L.-J.","year":"2008","unstructured":"L.-J. Guillemette and S. Monnier . One vote for type families in Haskell! In Proc . 9th Symposium on Trends in Functional Programming , 2008 b. L.-J. Guillemette and S. Monnier. One vote for type families in Haskell! In Proc. 9th Symposium on Trends in Functional Programming, 2008b."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645867.670933"},{"key":"e_1_3_2_1_19_1","first-page":"71","volume-title":"Proc. 2001 ACM SIGPLAN Workshop on Haskell, Haskell '01","author":"Kahl W.","year":"2001","unstructured":"W. Kahl and J. Scheffczyk . Named instances for Haskell type classes . In Proc. 2001 ACM SIGPLAN Workshop on Haskell, Haskell '01 , pages 71 -- 99 . ACM, 2001 . See also: http:\/\/ist.unibw-muenchen.de\/Haskell\/NamedInstances\/. W. Kahl and J. Scheffczyk. Named instances for Haskell type classes. In Proc. 2001 ACM SIGPLAN Workshop on Haskell, Haskell '01, pages 71--99. ACM, 2001. See also: http:\/\/ist.unibw-muenchen.de\/Haskell\/NamedInstances\/."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.10.039"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/331960.331977"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325708"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364394.2364397"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004355"},{"key":"e_1_3_2_1_26_1","unstructured":"C. McBride. Epigram 2004. http:\/\/www.dur.ac.uk\/CARG\/epigram.  C. McBride. Epigram 2004. http:\/\/www.dur.ac.uk\/CARG\/epigram."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707790.1707792"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581496"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317781"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411213"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596599"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_3_2_1_35_1","volume-title":"GADTs + extensible kind system = dependent programming. Technical report","author":"Sheard T.","year":"2005","unstructured":"T. Sheard , J. Hook , and N. Linger . GADTs + extensible kind system = dependent programming. Technical report , Portland State University , 2005 . http:\/\/www.cs.pdx.edu\/~sheard. T. Sheard, J. Hook, and N. Linger. GADTs + extensible kind system = dependent programming. Technical report, Portland State University, 2005. http:\/\/www.cs.pdx.edu\/~sheard."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364554"},{"key":"e_1_3_2_1_38_1","volume-title":"Down with kinds: adding dependent heterogeneous equality to FC (extended version). Technical report","author":"Weirich S.","year":"2012","unstructured":"S. Weirich , J. Hsu , and R. A. Eisenberg . Down with kinds: adding dependent heterogeneous equality to FC (extended version). Technical report , University of Pennsylvania , 2012 . URL http:\/\/www.cis.upenn.edu\/~sweirich\/papers\/nokinds-extended.pdf. S. Weirich, J. Hsu, and R. A. Eisenberg. Down with kinds: adding dependent heterogeneous equality to FC (extended version). Technical report, University of Pennsylvania, 2012. URL http:\/\/www.cis.upenn.edu\/~sweirich\/papers\/nokinds-extended.pdf."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103795"}],"event":{"name":"ICFP'12: ACM SIGPLAN International Conference on Functional Programming","location":"Copenhagen Denmark","acronym":"ICFP'12","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2012 Haskell Symposium"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2364506.2364522","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2364506.2364522","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:33:59Z","timestamp":1750224839000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2364506.2364522"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,13]]},"references-count":41,"alternative-id":["10.1145\/2364506.2364522","10.1145\/2364506"],"URL":"https:\/\/doi.org\/10.1145\/2364506.2364522","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2430532.2364522","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2012,9,13]]},"assertion":[{"value":"2012-09-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}