{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:45Z","timestamp":1774837845204,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540605799","type":"print"},{"value":"9783540477709","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60579-7_3","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T20:42:43Z","timestamp":1330288963000},"page":"39-59","source":"Crossref","is-referenced-by-count":58,"title":["Codifying guarded definitions with recursive schemes"],"prefix":"10.1007","author":[{"given":"Eduarde","family":"Gim\u00e9nez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"3_CR1","unstructured":"Peter Aczel. Non-Well-Founded Sets, volume 14 of CLSI Lecture Notes. 1988."},{"key":"3_CR2","unstructured":"H. Barendregt. Lambda Calculi with types. Technical Report 91-19, Catholic University of Nijmegen, 1991."},{"key":"3_CR3","unstructured":"T. Coquand. Metamathematical Investigations of a Calculus of Constructions. In P. Odifreddi, editor, Logic and Computer Science, volume 31 of The APIC series, pages 91\u2013122. Academic Press, 1990."},{"key":"3_CR4","unstructured":"Thierry Coquand. Pattern-Matching in type theory. In Bengt Nordstr\u00f6m, Kent Petersson, Gordon Plotkin, editor, Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages 71\u201384, 1992."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. Infinite objects in Type Theory. In Henk Barendregt, Tobias Nipkow, editor, Types for Proofs and Programs, pages 62\u201378. LNCS 806, 1993.","DOI":"10.1007\/3-540-58085-9_72"},{"key":"3_CR6","unstructured":"G. Dowek et al. The Coq Proof assistant user's guide \u2014 Version 5.8. Technical Report 154, INRIA Roquencourt, 1993."},{"key":"3_CR7","unstructured":"Herman Geuvers. Inductive and Coinductive types with iteration and recursion. In Bengt Nordstr\u00f6m, Kent Petersson, Gordon Plotkin, editor, Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages 193\u2013217, 1992."},{"key":"3_CR8","volume-title":"Technical report, Laboratoire de l'Informatique du Parall\u00e9lisme","author":"E. Gim\u00e9nez","year":"1994","unstructured":"E. Gim\u00e9nez. Codifying guarded definitions with recursive schemes. Technical report, Laboratoire de l'Informatique du Parall\u00e9lisme, ENS-Lyon, 1994."},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Francois Leclerc and Christine Paulin-Mohring. Programming with streams in Coq. A case study: the Sieve of Eratosthenes. In Henk Barendregt, Tobias Nipkow, editor, Types for Proofs and Programs, pages 191\u2013212. LNCS 806, 1993.","DOI":"10.1007\/3-540-58085-9_77"},{"key":"3_CR10","unstructured":"F.P. Mendier. Inductive Definitions in Type Theory. PhD thesis, Cornell University, 1987."},{"key":"3_CR11","unstructured":"Christine Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Universit\u00e9 Paris VII, 1989."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Christine Paulin-Mohring. Inductive definitions in the system Coq: Rules and Properties. In M. Bezem, J.F. Groote, editor, Proceedings of the TLCA, 1993.","DOI":"10.1007\/BFb0037116"},{"key":"3_CR13","unstructured":"Lawrence Paulson. Co-induction and Co-recursion in Higher-order Logic. Technical report, Computer Laboratory, University of Cambridge, 1993."},{"key":"3_CR14","unstructured":"Andrew M. Pitts. A co-induction principle for recursively defined domains. Technical Report 252, Computer Laboratory, University of Cambridge, April 1992."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60579-7_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:59:54Z","timestamp":1605646794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60579-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605799","9783540477709"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-60579-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}