{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:32:23Z","timestamp":1750307543932,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,8,30]],"date-time":"2009-08-30T00:00:00Z","timestamp":1251590400000},"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":[[2009,8,30]]},"DOI":"10.1145\/1596614.1596616","type":"proceedings-article","created":{"date-parts":[[2009,9,1]],"date-time":"2009-09-01T17:53:09Z","timestamp":1251827589000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Polytypic properties and proofs 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":[[2009,8,30]]},"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"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/985799.985801"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_8_1","volume-title":"April","author":"de Vries Edsko","year":"2009","unstructured":"Edsko de Vries . Coq-club archives: Question about guardedness in cofixpoint , April 2009 . http:\/\/logical.saclay.inria.fr\/coqpuma\/messages\/aa72f538ea88b2e7. Edsko de Vries. Coq-club archives: Question about guardedness in cofixpoint, April 2009. http:\/\/logical.saclay.inria.fr\/coqpuma\/messages\/aa72f538ea88b2e7."},{"key":"e_1_3_2_1_9_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/11776178","volume-title":"School on Datatype-Generic Programming","author":"Gibbons Jeremy","year":"2006","unstructured":"Jeremy Gibbons . Datatype-generic programming . In School on Datatype-Generic Programming , volume 4719 of Lecture Notes in Computer Science , pages 1 -- 71 . Springer-Verlag , 2006 . Jeremy Gibbons. Datatype-generic programming. In School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science, pages 1--71. Springer-Verlag, 2006."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/648085.747179"},{"key":"e_1_3_2_1_11_1","volume-title":"Generic Programs and Proofs. Habilitationsschrift","author":"Hinze Ralf","year":"2000","unstructured":"Ralf Hinze . Generic Programs and Proofs. Habilitationsschrift , Universitat Bonn , Germany , 2000 b. Ralf Hinze. Generic Programs and Proofs. Habilitationsschrift, Universitat 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 SIGPLAN 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 Proceedings of the 2000 ACM SIGPLAN Haskell Workshop, Electronic Notes in Theoretical Computer Science , Volume 41 .1. Elsevier Science , 2000 . Ralf Hinze and Simon Peyton Jones. Derivable type classes. In Proceedings of the 2000 ACM SIGPLAN Haskell Workshop, Electronic Notes in Theoretical Computer Science, Volume 41.1. Elsevier Science, 2000."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Ralf\n      Hinze\n     and \n      Andres\n      L\u00f6h\n    .\n  Generic programming now! In School on Datatype-Generic Programming volume \n  4719\n   of \n  Lecture Notes in Computer Science pages \n  150\n  --\n  208\n  . \n  Springer-Verlag 2006\n  .   Ralf Hinze and Andres L\u00f6h. Generic programming now! In School on Datatype-Generic Programming volume 4719 of Lecture Notes in Computer Science pages 150--208. Springer-Verlag 2006.","DOI":"10.1007\/978-3-540-76786-2_3"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.10.006"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.07.001"},{"key":"e_1_3_2_1_17_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 Loh . Comparing approaches to generic programming in Haskell . In School on Datatype-Generic Programming , volume 4719 of Lecture Notes in Computer Science , pages 72 -- 149 . Springer-Verlag , 2006 . Ralf Hinze, Johan Jeuring, and Andres Loh. Comparing approaches to generic programming in Haskell. In School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science, pages 72--149. Springer-Verlag, 2006."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263763"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/640136.604179"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/645772.667945"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/646540.759262"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_16"},{"key":"e_1_3_2_1_24_1","series-title":"Conferences in Research and Practice in Information Technology (CRPIT)","volume-title":"CATS'07: Theory of Computing","author":"Morris Peter","year":"2007","unstructured":"Peter Morris , Thorsten Altenkirch , and Neil Ghani . Constructing strictly positive families . In CATS'07: Theory of Computing , volume 65 of Conferences in Research and Practice in Information Technology (CRPIT) , 2007 . Peter Morris, Thorsten Altenkirch, and Neil Ghani. Constructing strictly positive families. In CATS'07: Theory of Computing, volume 65 of Conferences in Research and Practice in Information Technology (CRPIT), 2007."},{"key":"e_1_3_2_1_25_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_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/646526.694882"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411301"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596585"},{"key":"e_1_3_2_1_29_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 omega . In Spring School on Datatype-Generic Programming , volume 4719 of Lecture Notes in Computer Science . Springer-Verlag , 2007 . Tim Sheard. Generic programming in omega. In Spring School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science. Springer-Verlag, 2007."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411318.1411326"}],"event":{"name":"ICFP '09: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Edinburgh Scotland","acronym":"ICFP '09"},"container-title":["Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1596614.1596616","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1596614.1596616","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:23:28Z","timestamp":1750249408000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1596614.1596616"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8,30]]},"references-count":28,"alternative-id":["10.1145\/1596614.1596616","10.1145\/1596614"],"URL":"https:\/\/doi.org\/10.1145\/1596614.1596616","relation":{},"subject":[],"published":{"date-parts":[[2009,8,30]]},"assertion":[{"value":"2009-08-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}