{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:39Z","timestamp":1725540519368},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_33","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T06:45:27Z","timestamp":1258353927000},"page":"639-659","source":"Crossref","is-referenced-by-count":6,"title":["Circular Coinduction with Special Contexts"],"prefix":"10.1007","author":[{"given":"Dorel","family":"Lucanu","sequence":"first","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"8","key":"33_CR1","first-page":"157","volume":"14","author":"J. Ad\u00e1mek","year":"2005","unstructured":"Ad\u00e1mek, J.: Introduction to coalgebra. Theory and Applications of Categories\u00a014(8), 157\u2013199 (2005)","journal-title":"Theory and Applications of Categories"},{"key":"33_CR2","first-page":"1","volume-title":"SETA 1998","author":"J.-P. Allouche","year":"1999","unstructured":"Allouche, J.-P., Shallit, J.: The ubiquitous Prouhet-Thue-Morse sequence. In: SETA 1998, pp. 1\u201316. Springer, Heidelberg (1999)"},{"issue":"298","key":"33_CR3","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1016\/S0304-3975(02)00865-4","volume":"3","author":"M. Bidoit","year":"2003","unstructured":"Bidoit, M., Hennicker, R., Kurz, A.: Observational logic, constructor-based logic, and their duality. Theoretical Computer Science\u00a03(298), 471\u2013510 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"33_CR4","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1016\/S0304-3975(01)00333-4","volume":"275","author":"A. Bouhoula","year":"2002","unstructured":"Bouhoula, A., Rusinowitch, M.: Observational proofs by rewriting. Theoretical Computer Science\u00a0275(1-2), 675\u2013698 (2002)","journal-title":"Theoretical Computer Science"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: All about Maude - a high-performance logical framework, how to specify, program and verify systems in rewriting logic. In: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for Proofs and Programs","author":"T. Coquand","year":"1994","unstructured":"Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 62\u201378. Springer, Heidelberg (1994)"},{"key":"33_CR7","unstructured":"Dennis, L.: Proof Planning Coinduction. PhD thesis, Edinburgh University (1998)"},{"key":"33_CR8","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/3-540-63104-6_29","volume-title":"Automated Deduction - CADE-14","author":"L. Dennis","year":"1997","unstructured":"Dennis, L., Bundy, A., Green, I.: Using a generalisation critic to find bisimulations for coinductive proofs. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 276\u2013290. Springer, Heidelberg (1997)"},{"key":"33_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04293-9","volume-title":"Introduction to Process Algebra","author":"W. Fokkink","year":"2000","unstructured":"Fokkink, W.: Introduction to Process Algebra. Springer, Berlin (2000)"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/978-3-540-40020-2_12","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Goguen","year":"2003","unstructured":"Goguen, J., Lin, K., Ro\u015fu, G.: Conditional circular coinductive rewriting with case analysis. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol.\u00a02755, pp. 216\u2013232. Springer, Heidelberg (2003)"},{"issue":"1","key":"33_CR11","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S0304-3975(99)00275-3","volume":"245","author":"J. Goguen","year":"2000","unstructured":"Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science\u00a0245(1), 55\u2013101 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"33_CR12","first-page":"307","volume":"11","author":"J. Goguen","year":"1985","unstructured":"Goguen, J., Meseguer, J.: Completeness of Many-Sorted Equational Logic. Houston Journal of Mathematics\u00a011(3), 307\u2013334 (1985)","journal-title":"Houston Journal of Mathematics"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-3-540-31984-9_26","volume-title":"Fundamental Approaches to Software Engineering","author":"D. Hausmann","year":"2005","unstructured":"Hausmann, D., Mossakowski, T., Schr\u00f6der, L.: Iterative circular coinduction for CoCasl in Isabelle\/HOL. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 341\u2013356. Springer, Heidelberg (2005)"},{"key":"33_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/978-3-642-03741-2_30","volume-title":"CALCO 2009","author":"D. Lucanu","year":"2009","unstructured":"Lucanu, D., Goriac, E.-I., Caltais, G., Ro\u015fu, G.: CIRC: A behavioral verification tool based on circular coinduction. In: Lenisa, M., Kurz, A., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 433\u2013442. Springer, Heidelberg (2009)"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-73859-6_25","volume-title":"Algebra and Coalgebra in Computer Science","author":"D. Lucanu","year":"2007","unstructured":"Lucanu, D., Ro\u015fu, G.: Circ: A circular coinductive prover. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol.\u00a04624, pp. 372\u2013378. Springer, Heidelberg (2007)"},{"key":"33_CR16","first-page":"275","volume-title":"Logic Colloquium 1987","author":"J. Meseguer","year":"1989","unstructured":"Meseguer, J.: General logics. In: Ebbinghaus, H.D., et al. (eds.) Logic Colloquium 1987, pp. 275\u2013329. North Holland, Amsterdam (1989)"},{"issue":"3:6","key":"33_CR17","first-page":"1","volume":"4","author":"M. Niqui","year":"2008","unstructured":"Niqui, M.: Coinductive formal reasoning in exact real arithmetic. Logical Methods in Computer Science\u00a04(3:6), 1\u201340 (2008)","journal-title":"Logical Methods in Computer Science"},{"key":"33_CR18","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1093\/logcom\/7.2.175","volume":"7","author":"L.C. Paulson","year":"1997","unstructured":"Paulson, L.C.: Mechanizing coinduction and corecursion in higher-order logic. Logic and Computation\u00a07, 175\u2013204 (1997)","journal-title":"Logic and Computation"},{"key":"33_CR19","unstructured":"Ro\u015fu, G.: Hidden Logic. PhD thesis, University of California at San Diego (2000)"},{"key":"33_CR20","first-page":"184","volume-title":"ICFP 2006","author":"G. Ro\u015fu","year":"2006","unstructured":"Ro\u015fu, G.: Equality of streams is a \n                    \n                      \n                    \n                    $\\Pi_2^0$\n                  -complete problem. In: ICFP 2006, pp. 184\u2013191. ACM, New York (2006)"},{"key":"33_CR21","unstructured":"Ro\u015fu, G., Goguen, J.: Circular coinduction, Short paper. In: IJCAR 2001 (2001)"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-642-03741-2_10","volume-title":"CALCO 2009","author":"G. Ro\u015fu","year":"2009","unstructured":"Ro\u015fu, G., Lucanu, D.: Circular Coinduction \u2013 A Proof Theoretical Foundation. In: Lenisa, M., Kurz, A., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 127\u2013144. Springer, Heidelberg (2009)"},{"issue":"1-3","key":"33_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(02)00895-2","volume":"308","author":"J. Rutten","year":"2003","unstructured":"Rutten, J.: Behavioural Differential Equations: A Coinductive Calculus of Streams, Automata, and Power Series. Theoretical Computer Science\u00a0308(1-3), 1\u201353 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"33_CR24","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1017\/S0960129504004517","volume":"15","author":"J. Rutten","year":"2005","unstructured":"Rutten, J.: A coinductive calculus of streams. Mathematical Structures in Computer Science\u00a015(1), 93\u2013147 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"33_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-73445-1_23","volume-title":"Logic, Language, Information and Computation","author":"A. Silva","year":"2007","unstructured":"Silva, A., Rutten, J.: Behavioural differential equations and coinduction for binary trees. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol.\u00a04576, pp. 322\u2013336. Springer, Heidelberg (2007)"},{"key":"33_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"R.J. Glabbeek van","year":"1993","unstructured":"van Glabbeek, R.J.: The linear time - branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 66\u201381. Springer, Heidelberg (1993)"},{"key":"33_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-642-02348-4_12","volume-title":"RTA 2009","author":"H. Zantema","year":"2009","unstructured":"Zantema, H.: Well-definedness of streams by termination. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 164\u2013178. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T07:28:53Z","timestamp":1619767733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}