{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:19:43Z","timestamp":1781893183462,"version":"3.54.5"},"reference-count":59,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2005,7,13]],"date-time":"2005-07-13T00:00:00Z","timestamp":1121212800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite computations. To every type A we associate a type of partial elements Partial(A), coinductively generated by two constructors: the first, return(a) just returns an element a:A; the second, step(x), adds a computation step to a recursive element x:Partial(A). We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad.<\/jats:p>","DOI":"10.2168\/lmcs-1(2:1)2005","type":"journal-article","created":{"date-parts":[[2005,7,14]],"date-time":"2005-07-14T08:39:17Z","timestamp":1121330357000},"source":"Crossref","is-referenced-by-count":90,"title":["General Recursion via Coinductive Types"],"prefix":"10.46298","volume":"Volume 1, Issue 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1220-7706","authenticated-orcid":false,"given":"Venanzio","family":"Capretta","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2005,7,13]]},"reference":[{"key":"10.2168\/LMCS-1(2:1)2005_aczel:1988","unstructured":"Peter Aczel.Non-Well-Founded Sets. Number 14 in CSLI Lecture Notes. Stanford University, 1988."},{"key":"10.2168\/LMCS-1(2:1)2005_aczel:2002","doi-asserted-by":"crossref","unstructured":"Peter Aczel. Algebras and coalgebras. In Roland Backhouse, Roy Crole, and Jeremy Gibbons, editors,Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 ofLNCS, pages 79-88. Springer, 2002.","DOI":"10.1007\/3-540-47797-7_3"},{"key":"10.2168\/LMCS-1(2:1)2005_balaa\/bertot:2000","doi-asserted-by":"crossref","unstructured":"Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In J. Harrison and M. Aagaard, editors,Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 ofLecture Notes in Computer Science, pages 1-16. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44659-1_1"},{"key":"10.2168\/LMCS-1(2:1)2005_barendregt:1992","unstructured":"H. P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors,Handbook of Logic in Computer Science, Volume 2, pages 117-309. Oxford University Press, 1992."},{"key":"10.2168\/LMCS-1(2:1)2005_barendregt\/geuvers:2001","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50020-5"},{"key":"10.2168\/LMCS-1(2:1)2005_barthe\/coquand:2002","doi-asserted-by":"crossref","unstructured":"G. Barthe and T. Coquand. An introduction to dependent type theory. In G. Barthe, P. Dybjer, L. Pinto, and J. Saraiva, editors,Proceedings of APPSEM'00}, volume 2395 of {\\em LNCS. Springer, 2002. To appear.","DOI":"10.1007\/3-540-45699-6_1"},{"key":"10.2168\/LMCS-1(2:1)2005_BFGPU:2002","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"10.2168\/LMCS-1(2:1)2005_BCP:2003","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004501"},{"key":"10.2168\/LMCS-1(2:1)2005_bgp:2005","doi-asserted-by":"crossref","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, and Fernando Pastawski. Practical inference for type-based termination in a polymorphic setting. In Urzyczyn \\citetlca2005, pages 71-85.","DOI":"10.1007\/11417170_7"},{"key":"10.2168\/LMCS-1(2:1)2005_barwise\/moss:1996","unstructured":"Jon Barwise and Lawrence Moss.Vicious Circles. Number 60 in CSLI Lecture Notes. CSLI, Stanford, California, 1996."},{"key":"10.2168\/LMCS-1(2:1)2005_bhm:2002","doi-asserted-by":"crossref","unstructured":"Nick Benton, John Hughes, and Eugenio Moggi. Monads and effects. In Gilles Barthe, Peter Dybjer, Lu\u00eds Pinto, and Jo\u00e3o Saravia, editors,Applied Semantics}, volume 2395 ofLNCS, pages 42-122. Springer, 2002. International Summer School, {APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures.","DOI":"10.1007\/3-540-45699-6_2"},{"key":"10.2168\/LMCS-1(2:1)2005_bertot:2005","doi-asserted-by":"crossref","unstructured":"Yves Bertot. Fileters on coinductive streams, an application to eratosthenes' sieve. In Urzyczyn \\citetlca2005, pages 102-115.","DOI":"10.1007\/11417170_9"},{"key":"10.2168\/LMCS-1(2:1)2005_bcd:2002","doi-asserted-by":"crossref","unstructured":"Yves Bertot, Venanzio Capretta, and Kuntal Das Barman. Type-theoretic functional sematics. In V. A. Carreno, C. A. Munoz, and S. Tahar, editors,Theorem Proving in Higher Order Logics, volume 2410 ofLNCS, pages 83-97. Springer, 2002. 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002.","DOI":"10.1007\/3-540-45685-6_7"},{"issue":"1","key":"10.2168\/LMCS-1(2:1)2005_bove:2001","first-page":"22","volume":"8","author":"A. Bove","year":"2001","journal-title":"Nordic Journal of Computing"},{"key":"10.2168\/LMCS-1(2:1)2005_bove\/capretta:2001","doi-asserted-by":"crossref","unstructured":"Ana Bove and Venanzio Capretta. Nested general recursion and partiality in type theory. In Richard J. Boulton and Paul B. Jackson, editors,Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 ofLecture Notes in Computer Science, pages 121-135. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-44755-5_10"},{"key":"10.2168\/LMCS-1(2:1)2005_bove\/capretta:2005a","doi-asserted-by":"crossref","unstructured":"Ana Bove and Venanzio Capretta. Recursive functions with higher order domains. In Urzyczyn tlca2005, pages 116-130.","DOI":"10.1007\/11417170_10"},{"key":"10.2168\/LMCS-1(2:1)2005_capretta:1999","doi-asserted-by":"crossref","unstructured":"Venanzio Capretta. Universal algebra in type theory. In Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowits, Christine Paulin, and Laurent Th\u00e9ry, editors,Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs '99, volume 1690 ofLecture Notes in Computer Science, pages 131-148. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48256-3_10"},{"key":"10.2168\/LMCS-1(2:1)2005_capretta:2002","unstructured":"Venanzio Capretta.Abstraction and Computation. PhD thesis, Computing Science Institute, University of Nijmegen, 2002."},{"key":"10.2168\/LMCS-1(2:1)2005_constable:1986","unstructured":"R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith.Implementing Mathematics with the NuprlProof Development System. Prentice-Hall, 1986."},{"key":"10.2168\/LMCS-1(2:1)2005_constable:1983","doi-asserted-by":"crossref","unstructured":"Robert L. Constable. Partial functions in constructive formal theories. InTheoretical Computer Science, 6th GI-Conference, Dortmunt, volume 145 ofLNCS, pages 1-18, January 1983.","DOI":"10.1007\/BFb0036465"},{"key":"10.2168\/LMCS-1(2:1)2005_constable\/smith:1987","unstructured":"Robert L. Constable and Scott Fraser Smith. Partial object in constructive type theory. InLogic in Computer Science, Ithaca, New York, pages 183-193, Washington, D.C., June 1987. IEEE."},{"key":"10.2168\/LMCS-1(2:1)2005_coquand:1993","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. Infinite objects in type theory. In Henk Barendregt and Tobias Nipkow, editors,Types for Proofs and Programs. International Workshop TYPES'93, volume 806 ofLecture Notes in Computer Science, pages 62-78. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-58085-9_72"},{"key":"10.2168\/LMCS-1(2:1)2005_coquand\/huet:1988","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"10.2168\/LMCS-1(2:1)2005_coquand\/paulin:1990","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and Christine Paulin. Inductively defined types. In P. Martin-L\u00f6f, editor,Proceedings of Colog '88, volume 417 ofLNCS. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"10.2168\/LMCS-1(2:1)2005_dubois\/donzeau:1998","unstructured":"Catherine Dubois and V\u00e9ronique Vigui\u00e9 Donzeau-Gouge. A setp towards the mechanization of partial functions: domains as inductive predicates. Presented at CADE-15, Workshop on Mechanization of Partial Functions, 1998."},{"key":"10.2168\/LMCS-1(2:1)2005_geuvers:1992","unstructured":"Herman Geuvers. Inductive and coinductive types with iteration and recursion. In Bengt Nordstr\u00f6m, Kent Pettersson, and Gordon Plotkin, editors,Proccedings of the 1992 Workshop on Types for Proofs and Programs, B\\rastad, Sweden, June 1992, pages 193-217, 1992. \\verb+ftp:\/\/ftp.cs.chalmers.se\/+\\linebreak[0] \\verb+pub\/cs-reports\/baastad.92\/proc.dvi.Z+."},{"key":"10.2168\/LMCS-1(2:1)2005_geuvers:1993","unstructured":"Herman Geuvers.Logics and Type systems. PhD thesis, University of Nijmegen, September 1993."},{"key":"10.2168\/LMCS-1(2:1)2005_gpz:1999","doi-asserted-by":"crossref","unstructured":"Herman Geuvers, Erik Poll, and Jan Zwanenburg. Safe proof checking in type theory with Y. In F. Flum and M. Rodriguez-Artalejo, editors,Computer Science Logic (CSL'99), volume 1683 ofLNCS, pages 439-452. Stringer-Verlag, 1999.","DOI":"10.1007\/3-540-48168-0_31"},{"key":"10.2168\/LMCS-1(2:1)2005_gimenez:1994","doi-asserted-by":"crossref","unstructured":"Eduardo Gim\u00e9nez. Codifying guarded definitions with recursive schemes. In Peter Dybjer, Bengt Nordstr\u00f6m, and Jan Smith, editors,Types for Proofs and Programs. International Workshop TYPES '94, volume 996 ofLecture Notes in Computer Science, pages 39-59. Springer, 1994.","DOI":"10.1007\/3-540-60579-7_3"},{"key":"10.2168\/LMCS-1(2:1)2005_girard:1972","unstructured":"Jean-Yves Girard.Interpr\u00e9tation fonctionelle et \u00b4elimination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, 1972. These d'Etat."},{"key":"10.2168\/LMCS-1(2:1)2005_girard:1989","unstructured":"Jean-Yves Girard.Proofs and Types. Cambridge University Press, 1989. Translated and with appendices by Paul Taylor and Yves Lafont."},{"key":"10.2168\/LMCS-1(2:1)2005_hagino:1987a","unstructured":"Tatsuya Hagino.A Categorical Programming Language. PhD thesis, University of Edinburgh, 1987."},{"key":"10.2168\/LMCS-1(2:1)2005_hagino:1987","doi-asserted-by":"crossref","unstructured":"Tatsuya 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}, volume 283 of {\\em LNCS, pages 140-157. Springer, 1987.","DOI":"10.1007\/3-540-18508-9_24"},{"key":"10.2168\/LMCS-1(2:1)2005_hedberg:1996","doi-asserted-by":"publisher","DOI":"10.1007\/BF00252182"},{"key":"10.2168\/LMCS-1(2:1)2005_hermida\/jacobs:1998","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"10.2168\/LMCS-1(2:1)2005_howard:1980","unstructured":"W. A. Howard. The formulae-as-types notion of construction. In J. P. Selding and J. R. Hindley, editors,To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479-490. Academic Press, 1980."},{"key":"10.2168\/LMCS-1(2:1)2005_jacobs\/rutten:1997","first-page":"222","volume":"62","author":"Bart Jacobs and Jan Rutten","year":"1997","journal-title":"EATCS Bulletin"},{"key":"10.2168\/LMCS-1(2:1)2005_martin-loef:1982","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. InLogic, Methodology and Philosophy of Science, VI, 1979, pages 153-175. North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"10.2168\/LMCS-1(2:1)2005_martin-loef:1984","unstructured":"Per Martin-L\u00f6f.Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980."},{"key":"10.2168\/LMCS-1(2:1)2005_mcbride\/mckinna:2002","unstructured":"Conor McBride and James McKinna. The view from the left. draft paper, 2002."},{"key":"10.2168\/LMCS-1(2:1)2005_mpc:1986","unstructured":"N. P. Mendler, P. Panangaden, and R. L. Constable. Infinite objects in type theory. InProceedings, Symposium on Logic in Computer Science, pages 249-255, Cambridge, Massachussetts, 16-18 June 1986. IEEE Computer Society."},{"key":"10.2168\/LMCS-1(2:1)2005_mendler:1987","unstructured":"Paul Francis Mendler.Inductive Definition in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1987."},{"key":"10.2168\/LMCS-1(2:1)2005_milner:1980","doi-asserted-by":"crossref","unstructured":"Robin Milner.A Calculus of Communicating Systems, volume 92 ofLecture Notes in Computer Science. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"10.2168\/LMCS-1(2:1)2005_moggi:1989","doi-asserted-by":"crossref","unstructured":"Eugenio Moggi. Computational lambda-calculus and monads. InProceedings, Fourth Annual Symposium on Logic in Computer Science (LICS), pages 14-23. IEEE Computer Society Press, 1989.","DOI":"10.1109\/LICS.1989.39155"},{"key":"10.2168\/LMCS-1(2:1)2005_moggi:1991","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"10.2168\/LMCS-1(2:1)2005_nordstrom:1988","doi-asserted-by":"publisher","DOI":"10.1007\/BF01941137"},{"key":"10.2168\/LMCS-1(2:1)2005_nps:1990","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith.Programming in Martin-L\u00f6f's Type Theory. An Introduction, volume 7 ofInternational Series of Monographs on Computer Scence. Oxford University Press, 1990."},{"key":"10.2168\/LMCS-1(2:1)2005_paulin:1993","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System {Coq - Rules and Properties}. In M. Bezem and J.-F. Groote, editors,Proceedings of the conference Typed Lambda Calculi and Applications, volume 664 ofLNCS, 1993. LIP research report 92-49.","DOI":"10.1007\/BFb0037116"},{"key":"10.2168\/LMCS-1(2:1)2005_paulson:1986b","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80002-5"},{"key":"10.2168\/LMCS-1(2:1)2005_pfenning\/paulin:1990","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus of Constructions. InProceedings of Mathematical Foundations of Programming Semantics, volume 442 ofLNCS. Springer-Verlag, 1990. technical report CMU-CS-89-209.","DOI":"10.1007\/BFb0040259"},{"key":"10.2168\/LMCS-1(2:1)2005_phillips:1992","doi-asserted-by":"crossref","unstructured":"J. C. C. Phillips. Recursion theory. InHandbook of Logic in Computer Science. Volume 1. Background: Mathematical Structures, pages 79-187. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537359.003.0002"},{"key":"10.2168\/LMCS-1(2:1)2005_reynolds:1993","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019459"},{"key":"10.2168\/LMCS-1(2:1)2005_scott:1982","doi-asserted-by":"crossref","unstructured":"Dana Scott. Domains for denotational semantics. In M. Nielsen and E. M. Schmidt, editors,Automata, Languages and Programming. Ninth Colloquium, volume 140 ofLecture Notes in Computer Science, pages 577-613. Springer-Verlag, 1982.","DOI":"10.1007\/BFb0012801"},{"key":"10.2168\/LMCS-1(2:1)2005_sorensen\/urzyczyn:1998","unstructured":"Morten Heine B. S\u00f8rensen and P. Urzyczyn. Lectures on the Curry-Howard isomorphism. Available as DIKU Rapport 98\/14, 1998."},{"key":"10.2168\/LMCS-1(2:1)2005_coq:2002","unstructured":"The Coq Development Team. LogiCal Project.The Coq Proof Assistant. Reference Manual. Version 7.3 1. INRIA, 2002."},{"key":"10.2168\/LMCS-1(2:1)2005_coq","unstructured":"The Coq Development Team. LogiCal Project.The Coq Proof Assistant. Reference Manual. Version 8. INRIA, 2004. Available at the web page \\verb+http:\/\/pauillac.inria.fr\/coq\/coq-eng.html+."},{"key":"10.2168\/LMCS-1(2:1)2005_tlca2005","unstructured":"Pawe\\l Urzyczyn, editor.Typed Lambda Calculi and Applications. 7th International Conference, TLCA2005, Nara, Japan, April 2005, volume 3461 ofLNCS. Springer, 2005. Benjamin Werner.M\u00e9ta-th\u00e9orie du Calcul des Constructions Inductives. PhD thesis, Universit\u00e9 Paris 7, 1994."},{"key":"10.2168\/LMCS-1(2:1)2005_winskel:1993","doi-asserted-by":"crossref","unstructured":"Glynn Winskel.The Formal Semantics of Programming Languages. The MIT Press, 1993.","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"10.2168\/LMCS-1(2:1)2005_wraith:1989","doi-asserted-by":"crossref","unstructured":"G. C. Wraith. A note on categorical datatypes. In D. H. Pitt, D. E. Rydehead, P. Dybjer, A. M. Pitts, and A. Poign\u00e9, editors,Category Theory and Computer Science, volume 389 ofLecture Notes in Computer Science, pages 118-127. Springer-Verlag, 1989.","DOI":"10.1007\/BFb0018348"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2265\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2265\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,27]],"date-time":"2024-01-27T21:57:47Z","timestamp":1706392667000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2265"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7,13]]},"references-count":59,"URL":"https:\/\/doi.org\/10.2168\/lmcs-1(2:1)2005","relation":{"references":[{"id-type":"doi","id":"10.1007\/3-540-44755-5_10","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"cs\/0505037","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0505037","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,7,13]]},"article-number":"2265"}}