{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T02:29:50Z","timestamp":1775096990529,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"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":[[2013,9,25]]},"DOI":"10.1145\/2500365.2500597","type":"proceedings-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T09:13:17Z","timestamp":1380100397000},"page":"197-208","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":40,"title":["Productive coprogramming with guarded recursion"],"prefix":"10.1145","author":[{"given":"Robert","family":"Atkey","sequence":"first","affiliation":[{"name":"Contemplate Ltd., Edinburgh, United Kingdom"}]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2013,9,25]]},"reference":[{"issue":"4","key":"e_1_3_2_1_1_1","first-page":"277","article-title":"Termination checking with types","volume":"38","author":"Abel A.","year":"2004","unstructured":"A. Abel . Termination checking with types . ITA , 38 ( 4 ): 277 -- 319 , 2004 . A. Abel. Termination checking with types. ITA, 38 (4): 277--319, 2004.","journal-title":"ITA"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264249"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.27"},{"key":"e_1_3_2_1_5_1","volume-title":"Presented at FICS","author":"Birkedal L.","year":"2010","unstructured":"L. Birkedal , J. Schwinghammer , and K. St\u00f8vring . A metric model of guarded recursion . In Presented at FICS 2010 , 2010. L. Birkedal, J. Schwinghammer, and K. St\u00f8vring. A metric model of guarded recursion. In Presented at FICS 2010, 2010."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_2_1_7_1","volume-title":"Computer Science, 1 (2)","author":"Capretta V.","year":"2005","unstructured":"V. Capretta . General recursion via coinductive types. Log. Meth . in Computer Science, 1 (2) , 2005 . V. Capretta. General recursion via coinductive types. Log. Meth. in Computer Science, 1 (2), 2005."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.43.3"},{"key":"e_1_3_2_1_9_1","volume-title":"Draft","author":"Danielsson N. A.","year":"2009","unstructured":"N. A. Danielsson and T. Altenkirch . Mixing induction and coinduction . Draft , 2009 . N. A. Danielsson and T. Altenkirch. Mixing induction and coinduction. Draft, 2009."},{"key":"e_1_3_2_1_10_1","volume-title":"Computer Science, 7 (2)","author":"Dreyer D.","year":"2011","unstructured":"D. Dreyer , A. Ahmed , and L. Birkedal . Logical step-indexed logical relations. Log. Meth . in Computer Science, 7 (2) , 2011 . D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. Log. Meth. in Computer Science, 7 (2), 2011."},{"key":"e_1_3_2_1_11_1","volume-title":"Computer Science, 5 (3)","author":"Ghani N.","year":"2009","unstructured":"N. Ghani , P. Hancock , and D. Pattinson . Representations of stream processors using nested fixed points. Log. Meth . in Computer Science, 5 (3) , 2009 . N. Ghani, P. Hancock, and D. Pattinson. Representations of stream processors using nested fixed points. Log. Meth. in Computer Science, 5 (3), 2009."},{"key":"e_1_3_2_1_12_1","volume-title":"International Workshop TYPES'94","volume":"996","author":"Gim\u00e9nez E.","year":"1994","unstructured":"E. Gim\u00e9nez . Codifying guarded definitions with recursive schemes. In Types for Proofs and Programs , International Workshop TYPES'94 , volume 996 of Lecture Notes in Computer Science, pages 39--59 , 1994 . E. Gim\u00e9nez. Codifying guarded definitions with recursive schemes. In Types for Proofs and Programs, International Workshop TYPES'94, volume 996 of Lecture Notes in Computer Science, pages 39--59, 1994."},{"key":"e_1_3_2_1_13_1","volume-title":"Representing contractive functions on streams. Submitted","author":"Hutton G.","year":"2011","unstructured":"G. Hutton and M. Jaskelioff . Representing contractive functions on streams. Submitted , 2011 . G. Hutton and M. Jaskelioff. Representing contractive functions on streams. Submitted, 2011."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034782"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.38"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178246"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(96)00021-8"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004154"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789002"},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. 9th Int. Conf.","volume":"802","author":"Pitts A. M.","year":"1994","unstructured":"A. M. Pitts . Computational adequacy via 'mixed' inductive definitions. In Mathematical Foundations of Programming Semantics , Proc. 9th Int. Conf. , volume 802 of Lecture Notes in Computer Science, pages 72--82. Springer-Verlag, Berlin , 1994 . A. M. Pitts. Computational adequacy via 'mixed' inductive definitions. In Mathematical Foundations of Programming Semantics, Proc. 9th Int. Conf., volume 802 of Lecture Notes in Computer Science, pages 72--82. Springer-Verlag, Berlin, 1994."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364550"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/0211062"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"}],"event":{"name":"ICFP'13: ACM SIGPLAN International Conference on Functional Programming","location":"Boston Massachusetts USA","acronym":"ICFP'13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","Northeastern University"]},"container-title":["Proceedings of the 18th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2500365.2500597","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2500365.2500597","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:34:32Z","timestamp":1750217672000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2500365.2500597"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,25]]},"references-count":24,"alternative-id":["10.1145\/2500365.2500597","10.1145\/2500365"],"URL":"https:\/\/doi.org\/10.1145\/2500365.2500597","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2544174.2500597","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,9,25]]},"assertion":[{"value":"2013-09-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}