{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:00Z","timestamp":1772164080740,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,9,4]],"date-time":"2016-09-04T00:00:00Z","timestamp":1472947200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003150","name":"Fonds Qu\u00e9b\u00e9cois de la Recherche sur la Nature et les Technologies","doi-asserted-by":"publisher","award":["B1"],"award-info":[{"award-number":["B1"]}],"id":[{"id":"10.13039\/501100003150","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["CGS D"],"award-info":[{"award-number":["CGS D"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,9,4]]},"DOI":"10.1145\/2951913.2951929","type":"proceedings-article","created":{"date-parts":[[2016,8,29]],"date-time":"2016-08-29T08:17:16Z","timestamp":1472458636000},"page":"351-363","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Indexed codata types"],"prefix":"10.1145","author":[{"given":"David","family":"Thibodeau","sequence":"first","affiliation":[{"name":"McGill University, Canada"}]},{"given":"Andrew","family":"Cave","sequence":"additional","affiliation":[{"name":"McGill University, Canada"}]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[{"name":"McGill University, Canada"}]}],"member":"320","published-online":{"date-parts":[[2016,9,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"e_1_3_2_1_3_1","unstructured":"Agda team. The Agda Wiki 2014.  Agda team. The Agda Wiki 2014."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071370"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_24"},{"issue":"2","key":"e_1_3_2_1_6_1","first-page":"1","article-title":"Abella: A system for reasoning about relational specifications","volume":"7","author":"Baelde D.","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_1_7_1","volume-title":"Chalmers University of Technology and University of G\u00f6teborg","author":"Betarte G.","year":"1998"},{"key":"e_1_3_2_1_8_1","series-title":"Lecture Notes in Computer Science (LNCS 3085)","first-page":"129","volume-title":"Types for Proofs and Programs (TYPES\u201903), Revised Selected Papers","author":"Brady E.","year":"2004"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103705"},{"key":"e_1_3_2_1_11_1","unstructured":"R.\n       \n      Cockett\n     and \n      \n      \n      T.\n       \n      Fukushima\n      \n  \n  . \n  About charity. Technical report Department of Computer Science The University of Calgary June\n   \n  1992\n  . Yellow Series Report No. 92\/480\/18. R. DeLine and M. F\u00e4hndrich. Typestates for objects. In 18th European Conference on Object-Oriented Programming (ECOOP 2004) Lecture Notes in Computer Science\n   \n  (LNCS\n   3086) pages 465\u2013\n  490\n  . Springer 2004.  R. Cockett and T. Fukushima. About charity. Technical report Department of Computer Science The University of Calgary June 1992. Yellow Series Report No. 92\/480\/18. R. DeLine and M. F\u00e4hndrich. Typestates for objects. In 18th European Conference on Object-Oriented Programming (ECOOP 2004) Lecture Notes in Computer Science (LNCS 3086) pages 465\u2013490. Springer 2004."},{"key":"e_1_3_2_1_12_1","series-title":"Lecture Notes in Computer Science","first-page":"540","volume-title":"K. Futatsugi, J.-P","author":"Goguen H."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"T. Hagino. A typed lambda calculus with categorical type constructors. In D. H. Pitt A. Poign\u00e9 and D. E. Rydeheard editors Category Theory and Computer Science Lecture Notes in Computer Science (LNCS 283) pages 140\u2013157. Springer 1987.   T. Hagino. A typed lambda calculus with categorical type constructors. In D. H. Pitt A. Poign\u00e9 and D. E. Rydeheard editors Category Theory and Computer Science Lecture Notes in Computer Science (LNCS 283) pages 140\u2013157. Springer 1987.","DOI":"10.1007\/3-540-18508-9_24"},{"key":"e_1_3_2_1_14_1","first-page":"115","volume-title":"Towards Practicable Foundations for Constructive Mathematics","author":"Hancock P.","year":"2005"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480927"},{"key":"e_1_3_2_1_17_1","unstructured":"P. B. Levy. Call-by-push-value. PhD thesis Queen Mary and Westfield College University of London 2001.  P. B. Levy. Call-by-push-value. PhD thesis Queen Mary and Westfield College University of London 2001."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.48"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1812941.1812953"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90033-X"},{"key":"e_1_3_2_1_22_1","volume-title":"McGill University","author":"Thibodeau D.","year":"2016"},{"key":"e_1_3_2_1_23_1","series-title":"Lecture Notes in Computer Science (LNCS 3085)","first-page":"408","volume-title":"Types for Proofs and Programs (TYPES\u201903), Revised Selected Papers","author":"Xi H."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328482"}],"event":{"name":"ICFP'16: ACM SIGPLAN International Conference on Functional Programming","location":"Nara Japan","acronym":"ICFP'16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951913.2951929","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2951913.2951929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:39:37Z","timestamp":1750203577000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951913.2951929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,4]]},"references-count":23,"alternative-id":["10.1145\/2951913.2951929","10.1145\/2951913"],"URL":"https:\/\/doi.org\/10.1145\/2951913.2951929","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3022670.2951929","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,9,4]]},"assertion":[{"value":"2016-09-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}