{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:06:40Z","timestamp":1774987600144,"version":"3.50.1"},"reference-count":37,"publisher":"Elsevier BV","issue":"5","license":[{"start":{"date-parts":[[2011,3,1]],"date-time":"2011-03-01T00:00:00Z","timestamp":1298937600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":881,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2011,3]]},"DOI":"10.1016\/j.entcs.2011.02.020","type":"journal-article","created":{"date-parts":[[2011,3,7]],"date-time":"2011-03-07T15:16:19Z","timestamp":1299510979000},"page":"135-157","source":"Crossref","is-referenced-by-count":8,"title":["The Recursion Scheme from the Cofree Recursive Comonad"],"prefix":"10.1016","volume":"229","author":[{"given":"Tarmo","family":"Uustalu","sequence":"first","affiliation":[]},{"given":"Varmo","family":"Vene","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/j.entcs.2011.02.020_br0010","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1051\/ita:2004015","article-title":"Termination checking with types","volume":"38","author":"Abel","year":"2004","journal-title":"Theor. Inform. and Appl."},{"issue":"1\u20133","key":"10.1016\/j.entcs.2011.02.020_br0020","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(02)00728-4","article-title":"Infinite trees and completely iterative theories: a coalgebraic view","volume":"300","author":"Aczel","year":"2003","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"10.1016\/j.entcs.2011.02.020_br0030","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1017\/S0960129502003900","article-title":"Generalised coinduction","volume":"13","author":"Bartels","year":"2003","journal-title":"Math. Struct. in Comput. Sci."},{"issue":"1","key":"10.1016\/j.entcs.2011.02.020_br0040","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1017\/S0960129503004122","article-title":"Type-based termination of recursive definitions","volume":"14","author":"Barthe","year":"2004","journal-title":"Math. Struct. in Comput. Sci."},{"key":"10.1016\/j.entcs.2011.02.020_br0050","series-title":"Proc. of 22nd IEEE Symp. on Logic in Comput. Sci.","first-page":"51","article-title":"Complete sequent calculi for induction and infinite descent","author":"Brotherston","year":"2007"},{"issue":"4","key":"10.1016\/j.entcs.2011.02.020_br0060","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1016\/j.ic.2005.08.005","article-title":"Recursive coalgebras from comonads","volume":"204","author":"Capretta","year":"2006","journal-title":"Inform. and Comput."},{"issue":"1","key":"10.1016\/j.entcs.2011.02.020_br0070","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1016\/S1571-0661(04)80904-6","article-title":"Deforestation, program transformation, and cut-elimination","volume":"44","author":"Cockett","year":"2001","journal-title":"Electron. Notes in Theor. Comput. Sci."},{"key":"10.1016\/j.entcs.2011.02.020_br0080","unstructured":"Cockett, R. and T. Fukushima, About Charity, Yellow Series Report 92\/480\/18, Dept. of Comput. Sci., Univ. of Calgary, 1992."},{"key":"10.1016\/j.entcs.2011.02.020_br0090","series-title":"Proc. of Int. Summer Category Theory Meeting","first-page":"141","article-title":"Strong categorical datatypes I","volume":"13","author":"Cockett","year":"1992"},{"key":"10.1016\/j.entcs.2011.02.020_br0100","unstructured":"de Bruin, P.J., \u201cInductive Types in Constructive Languages,\u201d PhD thesis, Dept. of Comput. Sci., Univ. of Groningen, 1995. Available at http:\/\/irs.ub.rug.nl\/ppn\/128570415."},{"key":"10.1016\/j.entcs.2011.02.020_br0110","series-title":"Reports of the Midwest Category Seminar IV","first-page":"126","article-title":"Dinatural transformations","volume":"137","author":"Dubuc","year":"1970"},{"key":"10.1016\/j.entcs.2011.02.020_br0120","series-title":"Informal Proc. of Wksh. on Types for Proofs and Programs","first-page":"193","article-title":"Inductive and coinductive types with iteration and recursion","author":"Geuvers","year":"1992"},{"issue":"2","key":"10.1016\/j.entcs.2011.02.020_br0130","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1017\/S0960129502003912","article-title":"Dualising initial algebras","volume":"13","author":"Ghani","year":"2003","journal-title":"Math. Structures in Comput. Sci."},{"key":"10.1016\/j.entcs.2011.02.020_br0140","series-title":"Proc. of 2nd Asian Symp. on Programming Languages and Systems","first-page":"327","article-title":"Build, augment and destroy, universally","volume":"3302","author":"Ghani","year":"2004"},{"key":"10.1016\/j.entcs.2011.02.020_br0150","series-title":"Proc. of 2nd Int. Conf. on Category Theory and Computer Science","first-page":"140","article-title":"A typed lambda calculus with categorical type constructors","volume":"283","author":"Hagino","year":"1987"},{"key":"10.1016\/j.entcs.2011.02.020_br0160","series-title":"Logic and Computer Science","first-page":"279","article-title":"Contracting proofs to programs","volume":"31","author":"Leivant","year":"1990"},{"key":"10.1016\/j.entcs.2011.02.020_br0170","unstructured":"Levy, P.B., T. Altenkirch et al., Polymorphic isomorphisms, discussion in the Types mailinglist, 2008. Available at http:\/\/lists.seas.upenn.edu\/pipermail\/types-list\/2008\/001179.html."},{"issue":"1","key":"10.1016\/j.entcs.2011.02.020_br0180","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1023\/A:1020831825964","article-title":"Tarski\u02bcs fixed-point theorem and lambda calculi with monotone inductive types","volume":"133","author":"Matthes","year":"2002","journal-title":"Synthese"},{"issue":"1\u20132","key":"10.1016\/j.entcs.2011.02.020_br0190","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","article-title":"Inductive types and type constraints in the second-order lambda-calculus","volume":"51","author":"Mendler","year":"1991","journal-title":"Ann. of Pure and Appl. Logic"},{"issue":"1","key":"10.1016\/j.entcs.2011.02.020_br0200","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2004.05.003","article-title":"Completely iterative algebras and completely iterative monads","volume":"196","author":"Milius","year":"2005","journal-title":"Inform. and Comput."},{"key":"10.1016\/j.entcs.2011.02.020_br0210","series-title":"Applications of Categories in Computer Science","first-page":"202","article-title":"Strong monads, algebras and fixed points","volume":"177","author":"Mulry","year":"1992"},{"issue":"2","key":"10.1016\/j.entcs.2011.02.020_br0220","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","article-title":"Recursive programming with proofs","volume":"94","author":"Parigot","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.entcs.2011.02.020_br0230","series-title":"Proc. of 15th Int. Conf. on Math. Foundations of Comput. Sci.","first-page":"464","article-title":"Investigation of finitary calculi for the temporal logics by means of infinitary calculi","volume":"452","author":"Pliuskevi\u010dius","year":"1990"},{"key":"10.1016\/j.entcs.2011.02.020_br0240","series-title":"Proc. of 5th Int. Conf. on Foundations of Software Science and Computation Structures","first-page":"357","article-title":"A calculus of circular proofs and its categorical semantics","volume":"2303","author":"Santocanale","year":"2002"},{"issue":"4","key":"10.1016\/j.entcs.2011.02.020_br0250","doi-asserted-by":"crossref","first-page":"1284","DOI":"10.2307\/2274279","article-title":"A natural extension of natural deduction","volume":"49","author":"Schroeder-Heister","year":"1984","journal-title":"J. of Symb. Logic"},{"key":"10.1016\/j.entcs.2011.02.020_br0260","unstructured":"Sp\u0142awski, Z., \u201cProof-Theoretic Approach to Inductive Definitions in ML-Like Programming Languages versus Second-Order Lambda Calculus,\u201d PhD thesis, Wroc\u0142aw Univ., 1993."},{"key":"10.1016\/j.entcs.2011.02.020_br0270","series-title":"Proc. of 6th Int. Conf. on Foundations of Software Science and Computational Structures","first-page":"425","article-title":"On the structure of inductive reasoning: circular and tree-shaped proofs in the \u03bc-calculus","volume":"2620","author":"Sprenger","year":"2003"},{"issue":"1","key":"10.1016\/j.entcs.2011.02.020_br0280","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","article-title":"Local model checking in the modal \u03bc-calculus","volume":"89","author":"Stirling","year":"1991","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.entcs.2011.02.020_br0290","series-title":"Proc. of 1st Int. Symp. on Functional Programming Languages in Education","first-page":"1","article-title":"Elementary strong functional programming","volume":"1022","author":"Turner","year":"1995"},{"issue":"7","key":"10.1016\/j.entcs.2011.02.020_br0300","first-page":"751","article-title":"Total functional programming","volume":"10","author":"Turner","year":"2004","journal-title":"J. of Univ. Comput. Sci."},{"key":"10.1016\/j.entcs.2011.02.020_br0310","unstructured":"Uustalu, T., Strong dinaturality and initial algebras, slides for NWPT \u02bc00, 2000. Available at http:\/\/www.ii.uib.no\/~nwpt00\/Proceedings\/Uustalu-slides.ps."},{"key":"10.1016\/j.entcs.2011.02.020_br0320","unstructured":"Uustalu, T. and V. Vene, A cube of proof systems for the intuitionistic predicate \u03bc,\u03bd-logic, in: M. Haveraaen and O. Owe, eds., \u201cSelected Papers from 8th Nordic Wksh. on Programming Theory, NWPT \u02bc96 (Oslo, Dec. 1996),\u201d Research Report 248, Dept. of Informatics, Univ. of Oslo, 1997, pp. 237\u2013247."},{"issue":"1","key":"10.1016\/j.entcs.2011.02.020_br0330","first-page":"5","article-title":"Primitive (co)recursion and course-of-value (co)iteration, categorically","volume":"10","author":"Uustalu","year":"1999","journal-title":"Informatica"},{"key":"10.1016\/j.entcs.2011.02.020_br0340","unstructured":"Uustalu, T. and V. Vene, Coding recursion \u00e0 la Mendler (extended abstract), in: J. Jeuring, ed., \u201cProc. of 2nd Wksh. on Generic Programming, WGP 2000 (Ponte de Lima, July 2000),\u201d Technical Report UU-CS-2000-19, Universiteit Utrecht, 2000, pp. 69\u201385."},{"key":"10.1016\/j.entcs.2011.02.020_br0350","series-title":"Trends in Functional Programming 3","first-page":"99","article-title":"The dual of substitution is redecoration","author":"Uustalu","year":"2002"},{"issue":"3","key":"10.1016\/j.entcs.2011.02.020_br0360","first-page":"366","article-title":"Recursion schemes from comonads","volume":"8","author":"Uustalu","year":"2001","journal-title":"Nordic J. of Comput."},{"issue":"1\u20132","key":"10.1016\/j.entcs.2011.02.020_br0370","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1006\/inco.1999.2836","article-title":"Completeness of Kozen\u02bcs axiomatization of the propositional \u03bc-calculus","volume":"157","author":"Wa\u0142ukiewicz","year":"2000","journal-title":"Inform. and Comput."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066111000570?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066111000570?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,12,4]],"date-time":"2018-12-04T01:52:25Z","timestamp":1543888345000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066111000570"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3]]},"references-count":37,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2011,3]]}},"alternative-id":["S1571066111000570"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2011.02.020","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2011,3]]}}}