{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:12:51Z","timestamp":1774987971501,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370632","type":"print"},{"value":"9783642370649","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37064-9_42","type":"book-chapter","created":{"date-parts":[[2013,3,15]],"date-time":"2013-03-15T08:07:12Z","timestamp":1363334832000},"page":"480-492","source":"Crossref","is-referenced-by-count":7,"title":["Coinductive Proof Techniques for Language Equivalence"],"prefix":"10.1007","author":[{"given":"Jurriaan","family":"Rot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcello","family":"Bonsangue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Rutten","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"42_CR1","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proc. POPL (to appear, 2013)"},{"key":"42_CR2","doi-asserted-by":"crossref","unstructured":"Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Logical Methods in Computer Science 8(1) (2012)","DOI":"10.2168\/LMCS-8(1:16)2012"},{"issue":"4","key":"42_CR3","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"J. Brzozowski","year":"1964","unstructured":"Brzozowski, J.: Derivatives of regular expressions. J. ACM\u00a011(4), 481\u2013494 (1964)","journal-title":"J. ACM"},{"key":"42_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/BFb0084788","volume-title":"CONCUR \u201992","author":"S. Christensen","year":"1992","unstructured":"Christensen, S., H\u00fcttel, H., Stirling, C.: Bisimulation Equivalence is Decidable for All Context-Free Processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 138\u2013147. Springer, Heidelberg (1992)"},{"key":"42_CR5","unstructured":"Conway, J.: Regular Algebra and Finite Machines. Chapman and Hall (1971)"},{"key":"42_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-25379-9_11","volume-title":"Certified Programs and Proofs","author":"T. Coquand","year":"2011","unstructured":"Coquand, T., Siles, V.: A Decision Procedure for Regular Expression Equivalence in Type Theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 119\u2013134. Springer, Heidelberg (2011)"},{"key":"42_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-31365-3_22","volume-title":"Automated Reasoning","author":"S. Foster","year":"2012","unstructured":"Foster, S., Struth, G.: Automated Analysis of Regular Algebra. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 271\u2013285. Springer, Heidelberg (2012)"},{"issue":"3","key":"42_CR8","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1145\/321127.321132","volume":"9","author":"S. Ginsburg","year":"1962","unstructured":"Ginsburg, S., Rice, H.: Two families of languages related to ALGOL. J. ACM\u00a09(3), 350\u2013371 (1962)","journal-title":"J. ACM"},{"key":"42_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/11548133_12","volume-title":"Algebra and Coalgebra in Computer Science","author":"C. Grabmayer","year":"2005","unstructured":"Grabmayer, C.: Using Proofs by Coinduction to Find \u201cTraditional\u201d Proofs. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol.\u00a03629, pp. 175\u2013193. Springer, Heidelberg (2005)"},{"key":"42_CR10","doi-asserted-by":"crossref","unstructured":"Henglein, F., Nielsen, L.: Regular expression containment: coinductive axiomatization and computational interpretation. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 385\u2013398. ACM (2011)","DOI":"10.1145\/1925844.1926429"},{"key":"42_CR11","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. In: LICS, pp. 214\u2013225. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151646"},{"key":"42_CR12","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s10817-011-9223-4","volume":"49","author":"A. Krauss","year":"2012","unstructured":"Krauss, A., Nipkow, T.: Proof pearl: Regular expression equivalence and relation algebra. J. Automated Reasoning\u00a049, 95\u2013106 (2012); published online March 2011","journal-title":"J. Automated Reasoning"},{"key":"42_CR13","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":"42_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communication Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communication Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"42_CR15","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R. Milner","year":"1983","unstructured":"Milner, R.: Calculi for synchrony and asynchrony. TCS\u00a025, 267\u2013310 (1983)","journal-title":"TCS"},{"key":"42_CR16","unstructured":"Okhotin, A.: Conjunctive and boolean grammars: the true general case of the context-free grammars, http:\/\/users.utu.fi\/aleokh\/papers\/boolean_survey.pdf"},{"key":"42_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D.M.R. Park","year":"1981","unstructured":"Park, D.M.R.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"42_CR18","doi-asserted-by":"crossref","unstructured":"Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: Advanced Topics in Bisimulation and Coinduction, pp. 233\u2013289. Cambridge University Press (2012)","DOI":"10.1017\/CBO9780511792588.007"},{"key":"42_CR19","unstructured":"Rot, J., Bonchi, F., Bonsangue, M., Pous, D., Rutten, J., Silva, A.: Enhanced coalgebraic bisimulation, http:\/\/www.liacs.nl\/~jrot\/up-to.pdf"},{"key":"42_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-35843-2_32","volume-title":"SOFSEM 2013: Theory and Practice of Computer Science","author":"J. Rot","year":"2013","unstructured":"Rot, J., Bonsangue, M., Rutten, J.: Coalgebraic Bisimulation-Up-To. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol.\u00a07741, pp. 369\u2013381. Springer, Heidelberg (2013)"},{"key":"42_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/BFb0055624","volume-title":"CONCUR \u201998 Concurrency Theory","author":"J.J.M.M. Rutten","year":"1998","unstructured":"Rutten, J.J.M.M.: Automata and Coinduction (An Exercise in Coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 194\u2013218. Springer, Heidelberg (1998)"},{"issue":"1","key":"42_CR22","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J. Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comp. Sci.\u00a0249(1), 3\u201380 (2000)","journal-title":"Theor. Comp. Sci."},{"issue":"1-3","key":"42_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. Theor. Comput. Sci.\u00a0308(1-3), 1\u201353 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"42_CR24","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. in Comp. Sci.\u00a08(5), 447\u2013479 (1998), http:\/\/dx.doi.org\/10.1017\/S0960129598002527","journal-title":"Math. Struct. in Comp. Sci."},{"key":"42_CR25","doi-asserted-by":"crossref","unstructured":"Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: LICS, pp. 280\u2013291. IEEE Computer Society (1997)","DOI":"10.1109\/LICS.1997.614955"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37064-9_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T00:38:40Z","timestamp":1745973520000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37064-9_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370632","9783642370649"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37064-9_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}