{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:33:14Z","timestamp":1648513994102},"reference-count":40,"publisher":"EDP Sciences","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["RAIRO-Theor. Inf. Appl."],"published-print":{"date-parts":[[2009,10]]},"DOI":"10.1051\/ita\/2009015","type":"journal-article","created":{"date-parts":[[2009,8,31]],"date-time":"2009-08-31T08:39:23Z","timestamp":1251707963000},"page":"703-766","source":"Crossref","is-referenced-by-count":1,"title":["Two extensions of system F with (co)iteration and primitive (co)recursion principles"],"prefix":"10.1051","volume":"43","author":[{"given":"Favio Ezequiel","family":"Miranda-Perea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"250","published-online":{"date-parts":[[2009,9,1]]},"reference":[{"key":"R1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.tcs.2004.10.017","volume":"333","author":"Abel","year":"2005","journal-title":"Theoret. Comput. Sci."},{"key":"R2","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"B\u00f6hm","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"R3","unstructured":"R.L. Crole, Categories for Types.Cambridge Mathematical Textbooks. Cambridge University Press (1993)."},{"key":"R4","unstructured":"M.A. Cunha, Recursion patterns as hylomorphisms. Technical Report DI-PURe-03.11.01, Department of Informatics, University of Minho (2003)."},{"key":"R5","doi-asserted-by":"crossref","unstructured":"B.A. Davey and H.A. Priestley,Introduction to Lattices and Order, 2nd edn. Cambridge University Press (2002).","DOI":"10.1017\/CBO9780511809088"},{"key":"R6","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0304-3975(93)90186-W","volume":"111","author":"Dybkj\u00e6r","year":"1991","journal-title":"Theoret. Comput. Sci."},{"key":"R7","unstructured":"H. Geuvers, Inductive and coinductive types with iteration and recursion. InProceedings of the 1992 workshop on types for proofs and programs, B\u00e5stad, Sweden. Edited by B. Nordstr\u00f6m, K. Petterson, G. Plotkin (1992) 183\u2013207. Available via http:\/\/www.cs.kun.nl\/ herman\/BRABasInf_RecTyp.ps.gz."},{"key":"R8","doi-asserted-by":"crossref","unstructured":"J. Gibbons and G. Jones, The under-appreciated unfold. InProceedings 3rd ACM SIGPLAN international conference on functional programming, Baltimore, Maryland (1998) 273\u2013279.","DOI":"10.1145\/291251.289455"},{"key":"R9","doi-asserted-by":"crossref","unstructured":"J.Y. Girard, Une extension de l'interpretation de G\u00f6del \u00e0 l'analyse, et son application \u00e0 l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types. Second Scandinavian Logic Symposium. Edited by J.E. Fenstad. North-Holland (1971) 63\u201392.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"R10","unstructured":"J.Y. Girard, Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithmetique d'ordre sup\u00e9rieur. Th\u00e8se de Doctorat d'\u00c9tat, Universit\u00e9 de Paris VII (1972)."},{"key":"R11","unstructured":"J.Y. Girard, Y. Lafont and P. Taylor, Proofs and Types.Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1989)."},{"key":"R12","doi-asserted-by":"crossref","unstructured":"J. Greiner, Programming with inductive and co-inductive types. Technical Report CMU-CS-92-109, Carnegie-Mellon University (1992)","DOI":"10.21236\/ADA249562"},{"key":"R13","doi-asserted-by":"crossref","unstructured":"T. Hagino, A typed lambda calculus with categorical type constructors. InCategory Theory and Computer Science. Edited by D.H. Pitt, A. Poign\u00e9 and D.E. Rydeheard.Lect. Notes Comput. Sci.283(1987).","DOI":"10.1007\/3-540-18508-9_24"},{"key":"R14","unstructured":"T. Hagino, A Categorical programming language. Ph.D. Thesis CST-47-87 (also published as ECS-LFCS-87-38). Department of Computer Science, University of Edinburgh (1987)."},{"key":"R15","first-page":"222","volume":"62","author":"Jacobs","year":"1997","journal-title":"EATCS Bull."},{"key":"R16","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/11783596_15","volume":"4014","author":"Kabanov","year":"2006","journal-title":"Lect. Notes Comput. Sci."},{"key":"R17","unstructured":"J.L. Krivine, Lambda-calculus, types and models.Ellis Horwood Series in Computers and their Applications. Ellis Horwood, Masson (1993)."},{"key":"R18","unstructured":"S. Mac Lane, Categories for the Working Mathematician, 2nd. edn., Vol.5.Graduate Texts in Mathematics. Springer Verlag (1998)."},{"key":"R19","unstructured":"R. Matthes, Extensions of system F by iteration and primitive recursion on monotone inductive types. Dissertation Universit\u00e4t M\u00fcnchen (1999). Available via http:\/\/www.tcs.informatik.uni-muenchen.de\/ matthes\/dissertation\/ matthesdiss.ps.gz"},{"key":"R20","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1051\/ita:1999120","volume":"33","author":"Matthes","year":"1999","journal-title":"RAIRO-Theor. Inf. Appl."},{"key":"R21","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/10703163_20","volume":"1584","author":"Matthes","year":"1999","journal-title":"Lect. Notes Comput. Sci."},{"key":"R22","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1007\/3-540-44802-0_42","volume":"2142","author":"Matthes","year":"2001","journal-title":"Lect. Notes Comput. Sci."},{"key":"R23","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/j.apal.2004.10.009","volume":"133","author":"Matthes","year":"2005","journal-title":"Ann. Pure Appl. Logic"},{"key":"R24","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/3540543961_7","volume":"523","author":"Meijer","year":"1991","journal-title":"Lect. Notes Comput. Sci."},{"key":"R25","unstructured":"N.P. Mendler, Recursive types and type constraints in second-order lambda calculus. InProceedings of the 2nd Annual Symposium on Logic in Computer Science, Ithaca, N.Y. IEEE Computer Society Press, Washington D.C. (1987) 30\u201336."},{"key":"R26","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"Mendler","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"R27","unstructured":"F.E. Miranda-Perea, On extensions of AF2 with monotone and clausular (co)inductive definitions. Ph.D. Thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Germany (2004)."},{"key":"R28","doi-asserted-by":"crossref","unstructured":"F.E. Miranda-Perea, Some remarks on type systems for course-of-value recursion. InProceedings of the third workshop on Logical and Semantic Frameworks with Applications (LSFA 2008). Electronic Notes in Theoretical Computer Science247(2009).","DOI":"10.1016\/j.entcs.2009.07.051"},{"key":"R29","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","volume":"94","author":"Parigot","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"R30","doi-asserted-by":"crossref","unstructured":"E. Poll and J. Zwanenburg, From algebras and coalgebras to dialgebras. InCoalgebraic Methods in Computer Science (CMCS'2001).Electronic Notes in Theoretical Computer Science44(2001).","DOI":"10.1016\/S1571-0661(04)80915-0"},{"key":"R31","unstructured":"J. Reynolds, Towards a theory of type structure. InProc. Colloque sur la Programmation. Edited by B. Robinet.Lect. Notes Comput. Sci.19(1974)."},{"key":"R32","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/BFb0055624","volume":"1466","author":"Rutten","year":"1998","journal-title":"Lect. Notes Comput. Sci."},{"key":"R33","doi-asserted-by":"crossref","unstructured":"Z. Sp\u0142awski and P. Urzyczyn, Type fixpoints: iterationvs.recursion. InProc. International Conference on Functional Programming. ACM Press (1999), pp 102\u2013113.","DOI":"10.1145\/317765.317789"},{"key":"R34","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/BFb0064875","volume":"453","author":"Tait","year":"1975","journal-title":"Lect. Notes Math."},{"key":"R35","first-page":"751","volume":"10","author":"Turner","year":"2004","journal-title":"J. Universal Comput. Sci."},{"key":"R36","first-page":"5","volume":"10","author":"Uustalu","year":"1999","journal-title":"Informatica"},{"key":"R37","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/S0304-3975(00)00355-8","volume":"272","author":"Uustalu","year":"2002","journal-title":"Theoret. Comput. Sci."},{"key":"R38","unstructured":"V. Vene, Categorical programming with inductive and coinductive types.Diss. Math. Univ. Tartuensis23, Univ. Tartu (2000)."},{"key":"R39","doi-asserted-by":"crossref","unstructured":"P. Wadler, Theorems for free. InProc. 4th international conference on functional programming languages and computer architecture. Imperial College, London (1989), pp 347\u2013359.","DOI":"10.1145\/99370.99404"},{"key":"R40","unstructured":"G.C. Wraith, A note on categorical datatypes. InCategory Theory and Computer Science. Edited by D. Pittset\u00a0al.Lect. Notes Comput. Sci.389(1989)."}],"container-title":["RAIRO - Theoretical Informatics and Applications"],"original-title":[],"link":[{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/2009015\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T08:37:10Z","timestamp":1558514230000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/2009015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9,1]]},"references-count":40,"journal-issue":{"issue":"4"},"alternative-id":["ita07003"],"URL":"https:\/\/doi.org\/10.1051\/ita\/2009015","relation":{},"ISSN":["0988-3754","1290-385X"],"issn-type":[{"value":"0988-3754","type":"print"},{"value":"1290-385X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9,1]]}}}