{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:34:21Z","timestamp":1750307661031,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,9,20]],"date-time":"2008-09-20T00:00:00Z","timestamp":1221868800000},"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":[[2008,9,20]]},"DOI":"10.1145\/1411318.1411326","type":"proceedings-article","created":{"date-parts":[[2008,9,23]],"date-time":"2008-09-23T13:39:01Z","timestamp":1222177141000},"page":"49-60","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Polytypic programming in COQ"],"prefix":"10.1145","author":[{"given":"Wendy","family":"Verbruggen","sequence":"first","affiliation":[{"name":"Trinity College Dublin, Dublin, Ireland"}]},{"given":"Edsko","family":"de Vries","sequence":"additional","affiliation":[{"name":"Trinity College Dublin, Dublin, Ireland"}]},{"given":"Arthur","family":"Hughes","sequence":"additional","affiliation":[{"name":"Trinity College Dublin, Dublin, Ireland"}]}],"member":"320","published-online":{"date-parts":[[2008,9,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2008.01.004"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/647100.717294"},{"issue":"4","key":"e_1_3_2_1_4_1","first-page":"265","article-title":"Universes for Generic Programs and Proofs","volume":"100","author":"Benke Marcin","year":"2003","unstructured":"Marcin Benke , Peter Dybjer , and Patrik Jansson . Universes for Generic Programs and Proofs in Dependent Type Theory. Nordic Journal of Computing , 100 ( 4 ):0 265 -- 289 , 2003 . Marcin Benke, Peter Dybjer, and Patrik Jansson. Universes for Generic Programs and Proofs in Dependent Type Theory. Nordic Journal of Computing, 100 (4):0 265--289, 2003.","journal-title":"Dependent Type Theory. Nordic Journal of Computing"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_6_1","volume-title":"Coq frequently asked questions (v8.1)","author":"Team Coq Development","year":"2008","unstructured":"Coq Development Team . Coq frequently asked questions (v8.1) , 2008 . http:\/\/coq.inria.fr\/doc-eng.html. Coq Development Team. Coq frequently asked questions (v8.1), 2008. http:\/\/coq.inria.fr\/doc-eng.html."},{"issue":"2","key":"e_1_3_2_1_7_1","first-page":"0","article-title":"The Calculus of Constructions","volume":"760","author":"Coquand Thierry","year":"1988","unstructured":"Thierry Coquand and G\u00e9rard Huet . The Calculus of Constructions . Information and Computation , 760 ( 2-3 ): 0 95--120, 1988 . ISSN 0890-5401. http:\/\/dx.doi.org\/10.1016\/0890-5401(88)90005-3. 10.1016\/0890-5401(88)90005-3 Thierry Coquand and G\u00e9rard Huet. The Calculus of Constructions. Information and Computation, 760 (2-3):0 95--120, 1988. ISSN 0890-5401. http:\/\/dx.doi.org\/10.1016\/0890-5401(88)90005-3.","journal-title":"Information and Computation"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90108-T"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Ralf\n      Hinze\n    .\n  Polytypic Values Possess Polykinded Types\n  . In Roland Backhouse and Jos\u00e9 Nuno Oliveira editors 5th International Conference on Mathematics of Program Construction (MPC \n  2000\n  ) volume \n  1837\n   of \n  Lecture Notes in Computer Science pages \n  2\n  --\n  27\n  . \n  Springer-Verlag 2000a.   Ralf Hinze. Polytypic Values Possess Polykinded Types. In Roland Backhouse and Jos\u00e9 Nuno Oliveira editors 5th International Conference on Mathematics of Program Construction (MPC 2000) volume 1837 of Lecture Notes in Computer Science pages 2--27. Springer-Verlag 2000a.","DOI":"10.1007\/10722010_2"},{"key":"e_1_3_2_1_11_1","volume-title":"Universit\u00e4t Bonn","author":"Hinze Ralf","year":"2000","unstructured":"Ralf Hinze . Generic Programs and Proofs. Habilitationsschrift , Universit\u00e4t Bonn , Germany , 2000 b. Ralf Hinze. Generic Programs and Proofs. Habilitationsschrift, Universit\u00e4t Bonn, Germany, 2000b."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006022"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 2000 ACM SIG-PLAN Haskell Workshop, Electronic Notes in Theoretical Computer Science","volume":"41","author":"Hinze Ralf","year":"2000","unstructured":"Ralf Hinze and Simon Peyton Jones . Derivable Type Classes. In Graham Hutton, editor , Proceedings of the 2000 ACM SIG-PLAN Haskell Workshop, Electronic Notes in Theoretical Computer Science , Volume 41 .1. Elsevier Science , 2000 . Ralf Hinze and Simon Peyton Jones. Derivable Type Classes. In Graham Hutton, editor, Proceedings of the 2000 ACM SIG-PLAN Haskell Workshop, Electronic Notes in Theoretical Computer Science, Volume 41.1. Elsevier Science, 2000."},{"volume-title":"Now!","author":"Hinze Ralf","key":"e_1_3_2_1_14_1","unstructured":"Ralf Hinze and Andres L\u00f6h . Generic Programming , Now! In Roland Backhouse , Jeremy Gibbons , Ralf Hinze, and Johan Jeuring, editors, School on Datatype-Generic Programming, 2006, volume 4719 of Lecture Notes in Computer Science, pages 150--208. Springer-Verlag, 2006a. Ralf Hinze and Andres L\u00f6h. Generic Programming, Now! In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, School on Datatype-Generic Programming, 2006, volume 4719 of Lecture Notes in Computer Science, pages 150--208. Springer-Verlag, 2006a."},{"key":"e_1_3_2_1_15_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/11783596_13","volume-title":"Tarmo Uustalu","author":"Hinze Ralf","year":"2006","unstructured":"Ralf Hinze and Andres L\u00f6h. \" Scrap Your Boilerplate\"' Revolutions. In Tarmo Uustalu , editor, Mathematics of Program Construction: 8th International Conference (MPC 2006 ), volume 4014 of Lecture Notes in Computer Science , pages 180 -- 208 . Springer-Verlag , 2006b. 10.1007\/11783596_13 Ralf Hinze and Andres L\u00f6h. \"Scrap Your Boilerplate\"' Revolutions. In Tarmo Uustalu, editor, Mathematics of Program Construction: 8th International Conference (MPC 2006), volume 4014 of Lecture Notes in Computer Science, pages 180--208. Springer-Verlag, 2006b. 10.1007\/11783596_13"},{"key":"e_1_3_2_1_16_1","series-title":"Lecture Notes in Computer Science","first-page":"72","volume-title":"School on Datatype-Generic Programming","author":"Hinze Ralf","year":"2006","unstructured":"Ralf Hinze , Johan Jeuring , and Andres L\u00f6h . Comparing Approaches to Generic Programming in Haskell . In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, School on Datatype-Generic Programming , 2006 , volume 4719 of Lecture Notes in Computer Science , pages 72 -- 149 . Springer-Verlag , 2006a. Ralf Hinze, Johan Jeuring, and Andres L\u00f6h. Comparing Approaches to Generic Programming in Haskell. In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, School on Datatype-Generic Programming, 2006, volume 4719 of Lecture Notes in Computer Science, pages 72--149. Springer-Verlag, 2006a."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_3"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671442"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263763"},{"key":"e_1_3_2_1_20_1","first-page":"26","volume-title":"ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'03)","author":"Lammel R\u00e4lf","year":"2003","unstructured":"R\u00e4lf Lammel and Simon Peyton Jones . Scrap Your Boilerplate: A Practical Design Pattern for Generic Programming . In ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'03) , volume 38 , pages 26 -- 37 . ACM Press , 2003 . 10.1145\/604174.604179 R\u00e4lf Lammel and Simon Peyton Jones. Scrap Your Boilerplate: A Practical Design Pattern for Generic Programming. In ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'03), volume 38, pages 26--37. ACM Press, 2003. 10.1145\/604174.604179"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086391"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_16"},{"key":"e_1_3_2_1_25_1","volume-title":"Conferences in Research and Practice in Information Technology (CRPIT)","volume":"65","author":"Morris Peter","year":"2007","unstructured":"Peter Morris , Thorsten Altenkirch , and Neil Ghani . Constructing Strictly Positive Families. In Joachim Gudmundsson and Barry Jay, editors, Theory of Computing (CATS 2007) , Conferences in Research and Practice in Information Technology (CRPIT) , Volume 65 , 2007 . Peter Morris, Thorsten Altenkirch, and Neil Ghani. Constructing Strictly Positive Families. In Joachim Gudmundsson and Barry Jay, editors, Theory of Computing (CATS 2007), Conferences in Research and Practice in Information Technology (CRPIT), Volume 65, 2007."},{"key":"e_1_3_2_1_26_1","volume-title":"Computing Science","author":"Norell Ulf","year":"2002","unstructured":"Ulf Norell . Functional generic programming and type theory. Master's thesis , Computing Science , Chalmers University of Technology , 2002 . Ulf Norell. Functional generic programming and type theory. Master's thesis, Computing Science, Chalmers University of Technology, 2002."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_3_2_1_28_1","volume-title":"Workshop on Generic Programming (WGP'98)","author":"Pfeifer Holger","year":"1998","unstructured":"Holger Pfeifer and Harald Rue\u00df . Polytypic Abstraction in Type Theory. In Roland Backhouse and Tim Sheard, editors , Workshop on Generic Programming (WGP'98) . June 1998 . Holger Pfeifer and Harald Rue\u00df. Polytypic Abstraction in Type Theory. In Roland Backhouse and Tim Sheard, editors, Workshop on Generic Programming (WGP'98). June 1998."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/646526.694882"},{"key":"e_1_3_2_1_30_1","series-title":"Lecture Notes in Computer Science","volume-title":"Spring School on Datatype-Generic Programming","author":"Sheard Tim","year":"2007","unstructured":"Tim Sheard . Generic Programming in mega . In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, Spring School on Datatype-Generic Programming , volume 4719 of Lecture Notes in Computer Science . Springer-Verlag , 2007 . Tim Sheard. Generic Programming in mega. In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, Spring School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science. Springer-Verlag, 2007."},{"key":"e_1_3_2_1_31_1","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"S\u00f8rensen M. H.","year":"2006","unstructured":"M. H. S\u00f8rensen and P. Urzyczyn . Lectures on the Curry-Howard Isomorphism . Elsevier , 2006 . M. H. S\u00f8rensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006."},{"key":"e_1_3_2_1_32_1","volume-title":"Coq sources for this paper","author":"Verbruggen Wendy","year":"2008","unstructured":"Wendy Verbruggen . Coq sources for this paper , 2008 . https:\/\/www.cs.tcd.ie\/verbruwj\/pub\/. Wendy Verbruggen. Coq sources for this paper, 2008. https:\/\/www.cs.tcd.ie\/verbruwj\/pub\/."}],"event":{"name":"ICFP08: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Victoria BC Canada","acronym":"ICFP08"},"container-title":["Proceedings of the ACM SIGPLAN workshop on Generic programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1411318.1411326","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1411318.1411326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:29Z","timestamp":1750253369000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1411318.1411326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,9,20]]},"references-count":29,"alternative-id":["10.1145\/1411318.1411326","10.1145\/1411318"],"URL":"https:\/\/doi.org\/10.1145\/1411318.1411326","relation":{},"subject":[],"published":{"date-parts":[[2008,9,20]]},"assertion":[{"value":"2008-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}