{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T09:46:58Z","timestamp":1751881618717},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120312"},{"type":"electronic","value":"9783642120329"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12032-9_9","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T01:07:56Z","timestamp":1268010476000},"page":"109-127","source":"Crossref","is-referenced-by-count":11,"title":["Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Popescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elsa L.","family":"Gunter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"BOBJ, http:\/\/cseweb.ucsd.edu\/groups\/tatami\/bobj"},{"key":"9_CR2","unstructured":"The Coq proof assistant, http:\/\/coq.inria.fr"},{"key":"9_CR3","unstructured":"Isabelle, http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle"},{"key":"9_CR4","unstructured":"Aceto, L., Cimini, M., Ingolfsdottir, A.: A bisimulation-based method for proving the validity of equations in GSOS languages. To appear in Electr. Proc. Theor. Comput. Sci."},{"issue":"2","key":"9_CR5","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1017\/S0960129502003900","volume":"13","author":"F. Bartels","year":"2003","unstructured":"Bartels, F.: Generalised coinduction. Math. Struct. Comp. Sci.\u00a013(2), 321\u2013348 (2003)","journal-title":"Math. Struct. Comp. Sci."},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1145\/200836.200876","volume":"42","author":"B. Bloom","year":"1995","unstructured":"Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can\u2019t be traced. J. ACM\u00a042(1), 232\u2013268 (1995)","journal-title":"J. ACM"},{"key":"9_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/11554554_8","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Brotherston","year":"2005","unstructured":"Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 78\u201392. Springer, Heidelberg (2005)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/3-540-44618-4_20","volume-title":"CONCUR 2000 - Concurrency Theory","author":"R. Bruni","year":"2000","unstructured":"Bruni, R., de Frutos-Escrig, D., Mart\u00ed-Oliet, N., Montanari, U.: Bisimilarity congruences for open terms and term graphs via Tile Logic. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 259\u2013274. Springer, Heidelberg (2000)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/3-540-48685-2_18","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"1999","unstructured":"Clavel, M., Dur\u00e1n, F.J., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: The Maude system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 240\u2013243. Springer, Heidelberg (1999)"},{"issue":"2","key":"9_CR10","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1093\/logcom\/12.2.255","volume":"12","author":"M. Dam","year":"2002","unstructured":"Dam, M., Gurov, D.: \u03bc-calculus with explicit points and approximations. J. Log. Comput.\u00a012(2), 255\u2013269 (2002)","journal-title":"J. Log. Comput."},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/0304-3975(85)90093-3","volume":"37","author":"R. Simone de","year":"1985","unstructured":"de Simone, R.: Higher-level synchronizing devices in MEIJE-SCCS. Theor. Comput. Sci.\u00a037, 245\u2013267 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR12","unstructured":"Doumenc, G., Madelaine, E., de Simone, R.: Proving process calculi translations in ECRINS: The pureLOTOS \u2192 MEIJE example. Technical Report RR1192, INRIA (1990), http:\/\/hal.archives-ouvertes.fr\/inria-00075367\/en\/"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-61780-9_67","volume-title":"Types for Proofs and Programs","author":"E. Gim\u00e9nez","year":"1996","unstructured":"Gim\u00e9nez, E.: An application of co-inductive types in Coq: Verification of the alternating bit protocol. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 135\u2013152. Springer, Heidelberg (1996)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Lin, K., Ro\u015fu, G.: Circular coinductive rewriting. In: ASE 2000, pp. 123\u2013132 (2000)","DOI":"10.1109\/ASE.2000.873657"},{"issue":"2","key":"9_CR15","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1016\/0890-5401(92)90013-6","volume":"100","author":"J.F. Groote","year":"1992","unstructured":"Groote, J.F., Vaandrager, F.: Structured operational semantics and bisimulation as a congruence. Inf. Comput.\u00a0100(2), 202\u2013260 (1992)","journal-title":"Inf. Comput."},{"key":"9_CR16","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)"},{"issue":"4","key":"9_CR17","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/BF01213531","volume":"8","author":"M. Hennessy","year":"1996","unstructured":"Hennessy, M., Lin, H.: Proof systems for message-passing process algebras. Formal Asp. Comput.\u00a08(4), 379\u2013407 (1996)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF00121261","volume":"8","author":"P. Inverardi","year":"1996","unstructured":"Inverardi, P., Priami, C.: Automatic verification of distributed systems: The process algebra approach. Formal Methods in System Design\u00a08(1), 7\u201338 (1996)","journal-title":"Formal Methods in System Design"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-642-03741-2_30","volume-title":"Algebra and Coalgebra in Computer Science","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: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 433\u2013442. Springer, Heidelberg (2009)"},{"key":"9_CR20","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":"9_CR21","unstructured":"Madelaine, E.: Verification tools from the CONCUR project, http:\/\/www-sop.inria.fr\/meije\/papers\/concur-tools"},{"issue":"1","key":"9_CR22","first-page":"50","volume":"1","author":"T.F. Melham","year":"1994","unstructured":"Melham, T.F.: A mechanized theory of the pi-calculus in HOL. Nord. J. Comput.\u00a01(1), 50\u201376 (1994)","journal-title":"Nord. J. Comput."},{"issue":"3","key":"9_CR23","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1016\/0022-0000(84)90023-0","volume":"28","author":"R. Milner","year":"1984","unstructured":"Milner, R.: A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci.\u00a028(3), 439\u2013466 (1984)","journal-title":"J. Comput. Syst. Sci."},{"key":"9_CR24","volume-title":"Communication and concurrency","author":"R. Milner","year":"1998","unstructured":"Milner, R.: Communication and concurrency. Prentice-Hall, Englewood Cliffs (1998)"},{"issue":"1","key":"9_CR25","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-009-9125-x","volume":"43","author":"R. Monroy","year":"2009","unstructured":"Monroy, R., Bundy, A., Green, I.: On process equivalence = equation solving in ccs. J. Autom. Reasoning\u00a043(1), 53\u201380 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"9_CR26","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/j.tcs.2006.12.019","volume":"373","author":"M.R. Mousavi","year":"2007","unstructured":"Mousavi, M.R., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theor. Comput. Sci.\u00a0373(3), 238\u2013272 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-03741-2_12","volume-title":"Algebra and Coalgebra in Computer Science","author":"A. Popescu","year":"2009","unstructured":"Popescu, A.: Weak bisimilarity coalgebraically. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 157\u2013172. Springer, Heidelberg (2009)"},{"key":"9_CR28","unstructured":"Popescu, A., Gunter, E.L.: Incremental pattern-based coinduction for process algebra and its Isabelle formalization. Technical Report, University of Illinosis, https:\/\/hdl.handle.net\/2142\/14858"},{"issue":"1-2","key":"9_CR29","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1006\/inco.1999.2818","volume":"156","author":"A. Rensink","year":"2000","unstructured":"Rensink, A.: Bisimilarity of open terms. Inf. Comput.\u00a0156(1-2), 345\u2013385 (2000)","journal-title":"Inf. Comput."},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"R\u00f6ckl, C., Hirschkoff, D.: A fully adequate shallow embedding of the \u03c0-calculus in Isabelle\/HOL with mechanized syntax analysis. J. Funct. Program.\u00a013(2) (2003)","DOI":"10.1017\/S0956796802004653"},{"key":"9_CR31","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":"Algebra and Coalgebra in Computer Science","author":"G. Ro\u015fu","year":"2009","unstructured":"Ro\u015fu, G., Lucanu, D.: Circular coinduction: A proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 127\u2013144. Springer, Heidelberg (2009)"},{"issue":"3","key":"9_CR32","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1017\/S096012950000147X","volume":"2","author":"J.J.M.M. Rutten","year":"1992","unstructured":"Rutten, J.J.M.M.: Processes as terms: Non-well-founded models for bisimulation. Math. Struct. Comp. Sci.\u00a02(3), 257\u2013275 (1992)","journal-title":"Math. Struct. Comp. Sci."},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Rutten, J.J.M.M.: Elements of stream calculus (an extensive exercise in coinduction). Electr. Notes Theor. Comput. Sci., 45 (2001)","DOI":"10.1016\/S1571-0661(04)80972-1"},{"issue":"5","key":"9_CR34","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1017\/S0960129598002527","volume":"8","author":"D. Sangiorgi","year":"1998","unstructured":"Sangiorgi, D.: On the bisimulation proof method. Math. Struct. Comp. Sci.\u00a08(5), 447\u2013479 (1998)","journal-title":"Math. Struct. Comp. Sci."},{"key":"9_CR35","unstructured":"Sangiorgi, D., Walker, D.: The \u03c0-calculus. A theory of mobile processes, Cambridge (2001)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12032-9_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:05Z","timestamp":1606186025000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12032-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120312","9783642120329"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12032-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}