{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:38Z","timestamp":1772163998661,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,1,26]],"date-time":"2011-01-26T00:00:00Z","timestamp":1296000000000},"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":[[2011,1,26]]},"DOI":"10.1145\/1926385.1926411","type":"proceedings-article","created":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T09:58:22Z","timestamp":1295863102000},"page":"227-240","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Generative type abstraction and type-level computation"],"prefix":"10.1145","author":[{"given":"Stephanie","family":"Weirich","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dimitrios","family":"Vytiniotis","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Peyton Jones","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,1,26]]},"reference":[{"issue":"4","key":"e_1_3_2_2_1_1","first-page":"265","article-title":"Universes for generic programs and proofs in dependent type theory","volume":"10","author":"Benke M.","year":"2003","unstructured":"M. Benke , P. Dybjer , and P. Jansson . Universes for generic programs and proofs in dependent type theory . Nordic J. of Computing , 10 ( 4 ): 265 -- 289 , 2003 . ISSN 1236--6064. M. Benke, P. Dybjer, and P. Jansson. Universes for generic programs and proofs in dependent type theory. Nordic J. of Computing, 10(4):265--289, 2003. ISSN 1236--6064.","journal-title":"Nordic J. of Computing"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040306"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_3_2_2_7_1","volume-title":"First-class phantom types. CUCIS TR2003--1901","author":"Cheney J.","year":"2003","unstructured":"J. Cheney and R. Hinze . First-class phantom types. CUCIS TR2003--1901 , Cornell University , 2003 . J. Cheney and R. Hinze. First-class phantom types. CUCIS TR2003--1901, Cornell University, 2003."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/357233.357238"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317906"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90066-B"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086372"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199475"},{"key":"e_1_3_2_2_16_1","first-page":"148","volume-title":"Proceedings of the Sixth International Conference on Mathematics of Program Construction (MPC 2002","author":"Hinze R.","year":"2002","unstructured":"R. Hinze , J. Jeuring , and A. Loeh . Type-indexed data types. In B. M. Eerke Boiten, editor , Proceedings of the Sixth International Conference on Mathematics of Program Construction (MPC 2002 ), pages 148 -- 174 , Dagstuhl, Germany , July 2002 . R. Hinze, J. Jeuring, and A. Loeh. Type-indexed data types. In B. M. Eerke Boiten, editor, Proceedings of the Sixth International Conference on Mathematics of Program Construction (MPC 2002), pages 148--174, Dagstuhl, Germany, July 2002."},{"key":"e_1_3_2_2_17_1","volume-title":"Springer","author":"Kiselyov O.","year":"2010","unstructured":"O. Kiselyov , S. Peyton Jones , and C. Shan . Springer , 2010 . O. Kiselyov, S. Peyton Jones, and C. Shan. Springer, 2010."},{"key":"e_1_3_2_2_18_1","unstructured":"Fun with type functions.  Fun with type functions."},{"key":"e_1_3_2_2_19_1","volume-title":"A formulation of dependent ML with explicit equality proofs","author":"Licata D. R.","year":"2005","unstructured":"D. R. Licata and R. Harper . A formulation of dependent ML with explicit equality proofs . Technical Report Carnegie Mellon University-CS-05--178, Carnegie Mellon University Department of Computer Science , 2005 . D. R. Licata and R. Harper. A formulation of dependent ML with explicit equality proofs. Technical Report Carnegie Mellon University-CS-05--178, Carnegie Mellon University Department of Computer Science, 2005."},{"key":"e_1_3_2_2_20_1","series-title":"Studies in Logic and the Foundations of Mathematics","first-page":"73","volume-title":"Proceedings of the Logic Colloquium","author":"Martin-L\u00f6f P.","year":"1973","unstructured":"P. Martin-L\u00f6f . An intuitionistic theory of types: Predicative part . In Proceedings of the Logic Colloquium , 1973 , volume 80 of Studies in Logic and the Foundations of Mathematics , pages 73 -- 118 . North-Holland , 1975. P. Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In Proceedings of the Logic Colloquium, 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73--118. North-Holland, 1975."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/549659"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480926"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596572"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803003010"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_3_2_2_26_1","volume-title":"Advanced Topics in Types and Programming Lan-guages","author":"Pierce B. C.","year":"2005","unstructured":"B. C. Pierce , editor. Advanced Topics in Types and Programming Lan-guages . MIT Press , 2005 . B. C. Pierce, editor. Advanced Topics in Types and Programming Lan-guages. MIT Press, 2005."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.019"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888274"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645815.668885"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411215"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053469"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_2_2_33_1","unstructured":"The Coq Team. Coq. URL http:\/\/coq.inria.fr.  The Coq Team. Coq. URL http:\/\/coq.inria.fr."},{"key":"e_1_3_2_2_34_1","unstructured":"D. Vytiniotis G. Washburn and S. Weirich. An open and shut typecase. I.  D. Vytiniotis G. Washburn and S. Weirich. An open and shut typecase. I."},{"key":"e_1_3_2_2_35_1","volume-title":"SIGPLAN Workshop in Types in Language Design and Implementation","author":"ACM","year":"2005","unstructured":"ACM SIGPLAN Workshop in Types in Language Design and Implementation , Long Beach, CA, USA , Jan. 2005 . ACM SIGPLAN Workshop in Types in Language Design and Implementation, Long Beach, CA, USA, Jan. 2005."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"}],"event":{"name":"POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Austin Texas USA","acronym":"POPL '11","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1926385.1926411","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1926385.1926411","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:59:51Z","timestamp":1750229991000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1926385.1926411"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,26]]},"references-count":35,"alternative-id":["10.1145\/1926385.1926411","10.1145\/1926385"],"URL":"https:\/\/doi.org\/10.1145\/1926385.1926411","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1925844.1926411","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2011,1,26]]},"assertion":[{"value":"2011-01-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}