{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:49:40Z","timestamp":1725562180579},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212980"},{"type":"electronic","value":"9783540247272"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24727-2_11","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T15:06:41Z","timestamp":1280761601000},"page":"136-150","source":"Crossref","is-referenced-by-count":8,"title":["Unifying Recursive and Co-recursive Definitions in Sheaf Categories"],"prefix":"10.1007","author":[{"given":"Pietro","family":"Di Gianantonio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marino","family":"Miculan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44659-1_1","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Balaa","year":"2000","unstructured":"Balaa, A., Bertot, Y.: Fix-point equations for well-founded recursion in type theory. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 1\u201316. Springer, Heidelberg (2000)"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Bove, A.: General recursion in type theory. In: [5], pp. 39\u201358","DOI":"10.1007\/3-540-39185-1_3"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/S0019-9958(82)91250-5","volume":"54","author":"J.W. Bakker de","year":"1982","unstructured":"de Bakker, J.W., Zucker, J.I.: Processes and the denotational semantics of concurrency. Information and Control\u00a054, 70\u2013120 (1982)","journal-title":"Information and Control"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Di Gianantonio, P., Miculan, M.: A unifying approachto recursive and corecursive definitions. In: [5], pp. 148\u2013161","DOI":"10.1007\/3-540-39185-1_9"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of TYPES 2002","year":"2003","unstructured":"Geuvers, H., Wiedijk, F. (eds.): Proceedings of TYPES 2002. LNCS, vol.\u00a02646. Springer, Heidelberg (2003)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-60579-7_3","volume-title":"Types for Proofs and Programs","author":"E. Gim\u00e9nez","year":"1995","unstructured":"Gim\u00e9nez, E.: Codifying guarded recursion definitions withrecursiv e schemes. In: Smith, J., Dybjer, P., Nordstr\u00f6m, B. (eds.) TYPES 1994. LNCS, vol.\u00a0996, pp. 39\u201359. Springer, Heidelberg (1995)"},{"key":"11_CR7","unstructured":"Gimenez, E.: A tutorial on recursive types in Coq. RT-0221, INRIA (1998)"},{"key":"11_CR8","unstructured":"INRIA. The Coq Proof Assistant (2003), http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"11_CR9","volume-title":"General Topology","author":"J.L. Kelley","year":"1975","unstructured":"Kelley, J.L.: General Topology. Springer, Heidelberg (1975)"},{"key":"11_CR10","series-title":"Cambridge studies in advanced mathematics","volume-title":"Introduction to higher order categorical logic","author":"J. Lambek","year":"1986","unstructured":"Lambek, J., Scott, P.J.: Introduction to higher order categorical logic. Cambridge studies in advanced mathematics, vol.\u00a07. Cambridge University Press, Cambridge (1986)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-48256-3_6","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Matthews","year":"1999","unstructured":"Matthews, J.: Recursive function definition over coinductive types. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 73\u201390. Springer, Heidelberg (1999)"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/BF01941137","volume":"28","author":"B. Nordstr\u00f6m","year":"1988","unstructured":"Nordstr\u00f6m, B.: Terminating general recursion. BIT\u00a028, 605\u2013619 (1988)","journal-title":"BIT"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq; rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 328\u2013345. Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24727-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T03:22:44Z","timestamp":1559359364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24727-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212980","9783540247272"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24727-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}