{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:55:38Z","timestamp":1760043338628,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,9,18]],"date-time":"2011-09-18T00:00:00Z","timestamp":1316304000000},"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,9,18]]},"DOI":"10.1145\/2036918.2036921","type":"proceedings-article","created":{"date-parts":[[2011,9,20]],"date-time":"2011-09-20T13:50:16Z","timestamp":1316526616000},"page":"13-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Modularising inductive families"],"prefix":"10.1145","author":[{"given":"Hsiang-Shang","family":"Ko","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Gibbons","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,9,18]]},"reference":[{"key":"e_1_3_2_2_1_1","first-page":"1","volume-title":"IFIP TC2\/WG2.1 Working Conference on Generic Programming","author":"Altenkirch T.","year":"2003"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"crossref","unstructured":"R.\n       \n      Atkey P.\n       \n      Johann and \n      \n      \n      N.\n       \n      Ghani\n      \n  \n  . \n  When is a type refinement an inductive type? In M. Hofmann editor Foundations of Software Science and Computational Structures volume \n  6604\n   of \n  Lecture Notes in Computer Science pages \n  72\n  --\n  87\n  . \n  Springer-Verlag 2011\n  .   R. Atkey P. Johann and N. Ghani. When is a type refinement an inductive type? In M. Hofmann editor Foundations of Software Science and Computational Structures volume 6604 of Lecture Notes in Computer Science pages 72--87. Springer-Verlag 2011.","DOI":"10.1007\/978-3-642-19805-2_6"},{"volume-title":"Chalmers University of Technology","year":"2011","author":"Bernardy J.-P.","key":"e_1_3_2_2_3_1"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","unstructured":"J.-P.\n       \n      Bernardy\n     and \n      \n      \n      M.\n       \n      Lasson\n      \n  \n  . \n  Realizability and parametricity in pure type systems. In M. Hofmann editor Foundations of Software Science and Computation Structures volume \n  6604\n   of \n  Lecture Notes in Computer Science pages \n  108\n  --\n  122\n  . \n  Springer-Verlag 2011\n  .   J.-P. Bernardy and M. Lasson. Realizability and parametricity in pure type systems. In M. Hofmann editor Foundations of Software Science and Computation Structures volume 6604 of Lecture Notes in Computer Science pages 108--122. Springer-Verlag 2011.","DOI":"10.1007\/978-3-642-19805-2_8"},{"volume-title":"Prentice-Hall","year":"1997","author":"Bird R.","key":"e_1_3_2_2_5_1"},{"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","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11783596_12"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269016"},{"volume-title":"Bibliopolis","year":"1984","author":"Martin-L\u00f6f P.","key":"e_1_3_2_2_10_1"},{"key":"e_1_3_2_2_11_1","unstructured":"C. McBride. Ornamental algebras algebraic ornaments. To appear in Journal of Functional Programming.  C. McBride. Ornamental algebras algebraic ornaments. To appear in Journal of Functional Programming."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707790.1707792"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"crossref","unstructured":"F.\n       \n      Nordvall Forsberg\n     and \n      \n      \n      A.\n       \n      Setzer\n      \n  \n  . \n  Inductive-inductive definitions. In A. Dawar and H. Veith editors Computer Science Logic volume \n  6247\n   of \n  Lecture Notes in Computer Science pages \n  454\n  --\n  468\n  . \n  Springer-Verlag 2010\n  .   F. Nordvall Forsberg and A. Setzer. Inductive-inductive definitions. In A. Dawar and H. Veith editors Computer Science Logic volume 6247 of Lecture Notes in Computer Science pages 454--468. Springer-Verlag 2010.","DOI":"10.1007\/978-3-642-15205-4_35"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"crossref","unstructured":"U.\n       \n      Norell\n    .\n      \n  \n   \n  Dependently typed programming in Agda. In P. Koopman R. Plasmeijer and D. Swierstra editors Advanced Functional Programming (AFP\n   \n  2008\n  ) volume \n  5832\n   of \n  Lecture Notes in Computer Science pages \n  230\n  --\n  266\n  . \n  Springer-Verlag 2009.   U. Norell. Dependently typed programming in Agda. In P. Koopman R. Plasmeijer and D. Swierstra editors Advanced Functional Programming (AFP 2008) volume 5832 of Lecture Notes in Computer Science pages 230--266. Springer-Verlag 2009.","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75285"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"event":{"name":"ICFP '11: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Tokyo Japan","acronym":"ICFP '11"},"container-title":["Proceedings of the seventh ACM SIGPLAN workshop on Generic programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2036918.2036921","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2036918.2036921","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:48:29Z","timestamp":1750240109000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2036918.2036921"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,18]]},"references-count":16,"alternative-id":["10.1145\/2036918.2036921","10.1145\/2036918"],"URL":"https:\/\/doi.org\/10.1145\/2036918.2036921","relation":{},"subject":[],"published":{"date-parts":[[2011,9,18]]},"assertion":[{"value":"2011-09-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}