{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:58:20Z","timestamp":1759147100279},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_42","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:15:38Z","timestamp":1180656938000},"page":"600-614","source":"Crossref","is-referenced-by-count":5,"title":["Monotone Inductive and Coinductive Constructors of Rank 2"],"prefix":"10.1007","author":[{"given":"Ralph","family":"Matthes","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"42_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/3-540-45413-6_5","volume-title":"Proceedings of TLCA 2001","author":"T. Altenkirch","year":"2001","unstructured":"Thorsten Altenkirch. Representations of first order function types as terminal coalgebras. In Samson Abramsky, editor, Proceedings of TLCA 2001, volume 2044 of Lecture Notes in Computer Science, pages 8\u201321. Springer Verlag, 2001."},{"key":"42_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/3-540-48168-0_32","volume-title":"Computer Science Logic, 13th International Workshop, CSL\u201999, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings","author":"T. Altenkirch","year":"1999","unstructured":"Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In J\u00f6rg Flum and Mario Rodr\u00fdguez-Artalejo, editors, Computer Science Logic, 13th International Workshop, CSL\u201999, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, volume 1683 of Lecture Notes in Computer Science, pages 453\u2013468. Springer Verlag, 1999."},{"issue":"1","key":"42_CR3","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1017\/S0956796899003366","volume":"9","author":"R. S. Bird","year":"1999","unstructured":"Richard S. Bird and Ross Paterson. De Bruijn notation as a nested datatype. Journal of Functional Programming, 9(1):77\u201391, 1999.","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"42_CR4","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/s001650050047","volume":"11","author":"R. Bird","year":"1999","unstructured":"Richard Bird and Ross Paterson. Generalised folds for nested datatypes. Formal Aspects of Computing, 11(2):200\u2013222, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"42_CR5","unstructured":"Herman Geuvers. Inductive and coinductive types with iteration and recursion. In Bengt Nordstr\u00f6m, Kent Pettersson, and Gordon Plotkin, editors, Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u2134astad, Sweden, June 1992, pages 193\u2013217, 1992. Only published electronically. Available at ftp:\/\/ftp.cs.chalmers.se\/pub\/cs-reports\/baastad.92\/proc.dvi.Z ."},{"key":"42_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/BFb0014052","volume-title":"Proceedings of the Second International Conference on Typed Lambda Calculi and Applications (TLCA\u2019 95), Edinburgh, United Kingdom, April 1995","author":"N. Ghani","year":"1995","unstructured":"Neil Ghani. \u03b2\u03b7-equality for coproducts. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications (TLCA\u2019 95), Edinburgh, United Kingdom, April 1995, volume 902 of Lecture Notes in Computer Science, pages 171\u2013185. Springer Verlag, 1995."},{"key":"42_CR7","unstructured":"Jean-Yves Girard. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de Doctorat d\u2019\u00c9tat, Universit\u00e8 de Paris VII, 1972."},{"key":"42_CR8","unstructured":"Brian Howard. Fixed Points and Extensionality in Typed Functional Programming Languages. PhD thesis, Stanford University, 1992."},{"key":"42_CR9","unstructured":"Daniel Leivant. Contracting proofs to programs. In Piergiorgio Odifreddi, editor, Logic and Computer Science, volume 31 of APIC Studies in Data Processing, pages 279\u2013327. Academic Press, 1990."},{"key":"42_CR10","unstructured":"Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Doktorarbeit (PhD thesis), University of Munich, 1998."},{"key":"42_CR11","unstructured":"Nax P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, N.Y., pages 30\u201336. IEEE Computer Society Press, 1987."},{"key":"42_CR12","doi-asserted-by":"crossref","unstructured":"Chris Okasaki. From fast exponentiation to square matrices: An adventure in types. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP\u2019 99), Paris, France, September 27-29, 1999, volume 34 of SIGPLAN Notices, pages 28\u201335. ACM, 1999.","DOI":"10.1145\/317765.317781"},{"key":"42_CR13","volume-title":"D\u00e9finitions Inductives en Th\u00e9orie des Types d\u2019Ordre Sup\u00e9rieur","author":"C. Paulin-Mohring","year":"1996","unstructured":"Christine Paulin-Mohring. D\u00e9finitions Inductives en Th\u00e9orie des Types d\u2019Ordre Sup\u00e9rieur. Habilitation \u00e0 diriger les recherches, ENS Lyon, 1996."},{"key":"42_CR14","doi-asserted-by":"crossref","unstructured":"ZdzisSlaw SpSlawski and PaweSl Urzyczyn. Type Fixpoints: Iteration vs. Recursion. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP\u2019 99), Paris, France, September 27-29, 1999, volume 34 of SIGPLAN Notices, pages 102\u2013113. ACM, 1999.","DOI":"10.1145\/317765.317789"},{"key":"42_CR15","doi-asserted-by":"crossref","unstructured":"Tarmo Uustalu and Varmo Vene. Least and greatest fixed points in intuitionistic natural deduction. Theoretical Computer Science. To appear.","DOI":"10.1016\/S0304-3975(00)00355-8"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:21:14Z","timestamp":1556450474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_42","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}