{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:07:32Z","timestamp":1750306052488,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,8,31]],"date-time":"2016-08-31T00:00:00Z","timestamp":1472601600000},"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":[[2016,8,31]]},"DOI":"10.1145\/3064899.3064900","type":"proceedings-article","created":{"date-parts":[[2017,4,24]],"date-time":"2017-04-24T12:26:08Z","timestamp":1493036768000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Contractive Functions on Infinite Data Structures"],"prefix":"10.1145","author":[{"given":"Venanzio","family":"Capretta","sequence":"first","affiliation":[{"name":"Functional Programming Lab, University of Nottingham, UK"}]},{"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"Functional Programming Lab, University of Nottingham, UK"}]},{"given":"Mauro","family":"Jaskelioff","sequence":"additional","affiliation":[{"name":"CIFASIS--CONICET, Universidad, Nacional de Rosario, Argentina"}]}],"member":"320","published-online":{"date-parts":[[2016,8,31]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Andreas Abel and Brigitte Pientka. 2013. Wellfounded recursion with copatterns: a unified approach to termination and productivity See [42] 185--196.  Andreas Abel and Brigitte Pientka. 2013. Wellfounded recursion with copatterns: a unified approach to termination and productivity See [42] 185--196.","key":"e_1_3_2_1_1_1","DOI":"10.1145\/2544174.2500591"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1145\/2429069.2429075"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1016\/j.tcs.2005.06.002"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1007\/3-540-45413-6_5"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","first-page":"445","DOI":"10.3233\/FI-1980-3405","article-title":"The metric space of infinite trees. Algebraic and topological properties","volume":"3","author":"Arnold Andr\u00e9","year":"1980","unstructured":"Andr\u00e9 Arnold and Maurice Nivat . 1980 . The metric space of infinite trees. Algebraic and topological properties . Fundam. Inform. 3 , 4 (1980), 445 -- 476 . Andr\u00e9 Arnold and Maurice Nivat. 1980. The metric space of infinite trees. Algebraic and topological properties. Fundam. Inform. 3, 4 (1980), 445--476.","journal-title":"Fundam. Inform."},{"doi-asserted-by":"crossref","unstructured":"Robert Atkey and Conor McBride. 2013. Productive coprogramming with guarded recursion See [42] 197--208.  Robert Atkey and Conor McBride. 2013. Productive coprogramming with guarded recursion See [42] 197--208.","key":"e_1_3_2_1_6_1","DOI":"10.1145\/2544174.2500597"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.4064\/fm-3-1-133-181"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1016\/j.apal.2004.10.001"},{"volume-title":"Reflections on Type Theory, Lambda Calculus, and the Mind, Erik Barendsen, Herman Geuvers, Venanzio Capretta, and Milad Niqui (Eds.). ICIS","author":"Capretta Venanzio","unstructured":"Venanzio Capretta . 2007. Common Knowledge as a Coinductive Modality . In Reflections on Type Theory, Lambda Calculus, and the Mind, Erik Barendsen, Herman Geuvers, Venanzio Capretta, and Milad Niqui (Eds.). ICIS , Faculty of Science, Radbout University Nijmegen , 51--61. Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday. Venanzio Capretta. 2007. Common Knowledge as a Coinductive Modality. In Reflections on Type Theory, Lambda Calculus, and the Mind, Erik Barendsen, Herman Geuvers, Venanzio Capretta, and Milad Niqui (Eds.). ICIS, Faculty of Science, Radbout University Nijmegen, 51--61. Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday.","key":"e_1_3_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1016\/j.entcs.2010.08.015"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1016\/j.tcs.2011.04.024"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1093\/comjnl\/bxp004"},{"key":"e_1_3_2_1_13_1","volume-title":"Infinite Objects in Type Theory. In Types for Proofs and Programs. International Workshop TYPES'93 (Lecture Notes in Computer Science), Henk Barendregt and Tobias Nipkow (Eds.)","volume":"806","author":"Coquand Thierry","year":"1993","unstructured":"Thierry Coquand . 1993 . Infinite Objects in Type Theory. In Types for Proofs and Programs. International Workshop TYPES'93 (Lecture Notes in Computer Science), Henk Barendregt and Tobias Nipkow (Eds.) , Vol. 806 . Springer-Verlag, 62--78. Thierry Coquand. 1993. Infinite Objects in Type Theory. In Types for Proofs and Programs. International Workshop TYPES'93 (Lecture Notes in Computer Science), Henk Barendregt and Tobias Nipkow (Eds.), Vol. 806. Springer-Verlag, 62--78."},{"volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra . 1976. A Discipline of Programming . Prentice-Hall . Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall.","key":"e_1_3_2_1_14_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.2307\/2586554"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1007\/3-540-48959-2_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1016\/S0168-0072(02)00096-9"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_18_1","DOI":"10.1016\/j.tcs.2009.10.014"},{"key":"e_1_3_2_1_19_1","volume-title":"Types for Proofs and Programs","author":"Gambino Nicola","year":"2003","unstructured":"Nicola Gambino and Martin Hyland . 2003. Wellfounded Trees and Dependent Polynomial Functors . In Types for Proofs and Programs , International Workshop, TYPES 2003 , Torino, Italy, April 30-May 4, 2003, Revised Selected Papers (Lecture Notes in Computer Science), Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.), Vol. 3085 . Springer , 210--225. Nicola Gambino and Martin Hyland. 2003. Wellfounded Trees and Dependent Polynomial Functors. In Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30-May 4, 2003, Revised Selected Papers (Lecture Notes in Computer Science), Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.), Vol. 3085. Springer, 210--225."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1016\/j.entcs.2006.06.009"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1016\/j.entcs.2009.07.081"},{"key":"e_1_3_2_1_22_1","volume-title":"Representations of Stream Processors Using Nested Fixed Points. Logical Methods in Computer Science 5, 3","author":"Ghani Neil","year":"2009","unstructured":"Neil Ghani , Peter Hancock , and Dirk Pattinson . 2009. Representations of Stream Processors Using Nested Fixed Points. Logical Methods in Computer Science 5, 3 ( 2009 ). Neil Ghani, Peter Hancock, and Dirk Pattinson. 2009. Representations of Stream Processors Using Nested Fixed Points. Logical Methods in Computer Science 5, 3 (2009)."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1007\/3-540-39185-1_9"},{"volume-title":"Proc. FOSSACS'04 (LNCS)","author":"Gianantonio Pietro Di","unstructured":"Pietro Di Gianantonio and Marino Miculan . 2004. Unifying Recursive and Corecursive Definitions in Sheaf Categories . In Proc. FOSSACS'04 (LNCS) , Igor Walukiewicz (Ed.), Vol. 2987 . Springer , 136--150. Pietro Di Gianantonio and Marino Miculan. 2004. Unifying Recursive and Corecursive Definitions in Sheaf Categories. In Proc. FOSSACS'04 (LNCS), Igor Walukiewicz (Ed.), Vol. 2987. Springer, 136--150.","key":"e_1_3_2_1_24_1"},{"key":"e_1_3_2_1_25_1","first-page":"353","article-title":"Proof Methods for Corecursive Programs","volume":"66","author":"Gibbons Jeremy","year":"2005","unstructured":"Jeremy Gibbons and Graham Hutton . 2005 . Proof Methods for Corecursive Programs . Fundam. Inform. 66 , 4 (2005), 353 -- 366 . Jeremy Gibbons and Graham Hutton. 2005. Proof Methods for Corecursive Programs. Fundam. Inform. 66, 4 (2005), 353--366.","journal-title":"Fundam. Inform."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_26_1","DOI":"10.1145\/289423.289455"},{"key":"e_1_3_2_1_27_1","volume-title":"Types for Proofs and Programs. International Workshop TYPES '94 (Lecture Notes in Computer Science), Peter Dybjer, Bengt Nordstr\u00f6m, and Jan Smith (Eds.)","volume":"996","author":"Gim\u00e9nez Eduardo","year":"1994","unstructured":"Eduardo Gim\u00e9nez . 1994 . Codifying guarded definitions with recursive schemes . In Types for Proofs and Programs. International Workshop TYPES '94 (Lecture Notes in Computer Science), Peter Dybjer, Bengt Nordstr\u00f6m, and Jan Smith (Eds.) , Vol. 996 . Springer, 39--59. Eduardo Gim\u00e9nez. 1994. Codifying guarded definitions with recursive schemes. In Types for Proofs and Programs. International Workshop TYPES '94 (Lecture Notes in Computer Science), Peter Dybjer, Bengt Nordstr\u00f6m, and Jan Smith (Eds.), Vol. 996. Springer, 39--59."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.1016\/j.entcs.2006.06.003"},{"key":"e_1_3_2_1_29_1","first-page":"5","article-title":"Concrete stream calculus: An extended study","volume":"20","author":"Hinze Ralf","year":"2008","unstructured":"Ralf Hinze . 2008 . Concrete stream calculus: An extended study . J. Funct. Program. 20 , 5 - 6 (2008), 463--535. Ralf Hinze. 2008. Concrete stream calculus: An extended study. J. Funct. Program. 20, 5-6 (2008), 463--535.","journal-title":"J. Funct. Program."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1145\/1411204.1411232"},{"key":"e_1_3_2_1_31_1","first-page":"222","article-title":"A Tutorial on (Co)Algebras and (Co)Induction","volume":"62","author":"Jacobs Bart","year":"1997","unstructured":"Bart Jacobs and Jan Rutten . 1997 . A Tutorial on (Co)Algebras and (Co)Induction . Bulletin of the European Association for Theoretical Computer Science 62 (1997), 222 -- 259 . Bart Jacobs and Jan Rutten. 1997. A Tutorial on (Co)Algebras and (Co)Induction. Bulletin of the European Association for Theoretical Computer Science 62 (1997), 222--259.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"e_1_3_2_1_32_1","first-page":"222","article-title":"A Tutorial on (Co)Algebras and (Co)Induction","volume":"62","author":"Jacobs Bart","year":"1997","unstructured":"Bart Jacobs and Jan J. M. M. Rutten . 1997 . A Tutorial on (Co)Algebras and (Co)Induction . EATCS Bulletin 62 (1997), 222 -- 259 . Bart Jacobs and Jan J. M. M. Rutten. 1997. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin 62 (1997), 222--259.","journal-title":"EATCS Bulletin"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_33_1","DOI":"10.1109\/LICS.2011.38"},{"key":"e_1_3_2_1_34_1","volume-title":"CALCO 2015 (LIPIcs), Lawrence S. Moss and Pawel Sobocinski (Eds.)","volume":"35","author":"Kurz Alexander","year":"2015","unstructured":"Alexander Kurz , Alberto Pardo , Daniela Petrisan , Paula Severi , and Fer-Jan de Vries . 2015 . Approximation of Nested Fixpoints -- A Coalgebraic View of Parametric Dataypes . In CALCO 2015 (LIPIcs), Lawrence S. Moss and Pawel Sobocinski (Eds.) , Vol. 35 . Dagstuhl, Germany, 205--220. Alexander Kurz, Alberto Pardo, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. 2015. Approximation of Nested Fixpoints -- A Coalgebraic View of Parametric Dataypes. In CALCO 2015 (LIPIcs), Lawrence S. Moss and Pawel Sobocinski (Eds.), Vol. 35. Dagstuhl, Germany, 205--220."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.1007\/BF01110627"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_36_1","DOI":"10.1007\/978-3-319-08970-6_22"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.1145\/800017.800528"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_38_1","DOI":"10.1007\/3-540-48256-3_6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_39_1","DOI":"10.1109\/LICS.2012.57"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_40_1","DOI":"10.1007\/3540543961_7"},{"volume-title":"Proceedings, Symposium on Logic in Computer Science. IEEE Computer Society","author":"Mendler N. P.","unstructured":"N. P. Mendler , P. Panangaden , and R. L. Constable . 1986. Infinite Objects in Type Theory . In Proceedings, Symposium on Logic in Computer Science. IEEE Computer Society , Cambridge, Massachussetts, 249--255. N. P. Mendler, P. Panangaden, and R. L. Constable. 1986. Infinite Objects in Type Theory. In Proceedings, Symposium on Logic in Computer Science. IEEE Computer Society, Cambridge, Massachussetts, 249--255.","key":"e_1_3_2_1_41_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_42_1","DOI":"10.1145\/2500365"},{"volume-title":"A Modality for Recursion","author":"Nakano Hiroshi","unstructured":"Hiroshi Nakano . 2000. A Modality for Recursion . In LICS. IEEE Computer Society , 255--266. http:\/\/tinyurl.com\/huzq7gl Hiroshi Nakano. 2000. A Modality for Recursion. In LICS. IEEE Computer Society, 255--266. http:\/\/tinyurl.com\/huzq7gl","key":"e_1_3_2_1_43_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_44_1","DOI":"10.1016\/S0304-3975(02)00895-2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_45_1","DOI":"10.1017\/S0960129504004517"},{"doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi (Ed.). 2012. Advanced Topics in Bisimulation and Coinduction. Cambridge University Press.  Davide Sangiorgi (Ed.). 2012. Advanced Topics in Bisimulation and Coinduction. Cambridge University Press.","key":"e_1_3_2_1_46_1","DOI":"10.1017\/CBO9780511792588"},{"volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi Davide","unstructured":"Davide Sangiorgi . 2012. Introduction to Bisimulation and Coinduction . Cambridge University Press . Davide Sangiorgi. 2012. Introduction to Bisimulation and Coinduction. Cambridge University Press.","key":"e_1_3_2_1_47_1"},{"volume-title":"Handbook of Logic in Computer Science.","author":"Smyth M.B.","unstructured":"M.B. Smyth . 1992. Topology . In Handbook of Logic in Computer Science. Vol. 2 . Oxford University Press , 641--761. M.B. Smyth. 1992. Topology. In Handbook of Logic in Computer Science. Vol. 2. Oxford University Press, 641--761.","key":"e_1_3_2_1_48_1"}],"event":{"sponsor":["K.U. Leuven K.U. Leuven"],"acronym":"IFL 2016","name":"IFL 2016: Symposium on Implementation and Application of Functional Languages","location":"Leuven Belgium"},"container-title":["Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3064899.3064900","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3064899.3064900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:28Z","timestamp":1750215808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3064899.3064900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,31]]},"references-count":48,"alternative-id":["10.1145\/3064899.3064900","10.1145\/3064899"],"URL":"https:\/\/doi.org\/10.1145\/3064899.3064900","relation":{},"subject":[],"published":{"date-parts":[[2016,8,31]]},"assertion":[{"value":"2016-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}