{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:47:45Z","timestamp":1762458465887},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540638889"},{"type":"electronic","value":"9783540696612"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0000477","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T10:30:36Z","timestamp":1128508236000},"page":"276-291","source":"Crossref","is-referenced-by-count":13,"title":["Invariants, bisimulations and the correctness of coalgebraic refinements"],"prefix":"10.1007","author":[{"given":"Bart","family":"Jacobs","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,9,7]]},"reference":[{"key":"19_CR1","series-title":"number 389 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/BFb0018361","volume-title":"Category Theory and Computer Science","author":"P. Aczel","year":"1989","unstructured":"P. Aczel and N. Mendler. A final coalgebra theorem. In D.H. Pitt, A. Poign\u00e9, and D.E. Rydeheard, editors, Category Theory and Computer Science, number 389 in Lect. Notes Comp. Sci., pages 357\u2013365. Springer, Berlin, 1989."},{"key":"19_CR2","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/S0019-9958(82)80026-0","volume":"52","author":"M.A. Arbib","year":"1982","unstructured":"M.A. Arbib and E.G. Manes. Parametrized data types do not need highly constrained parameters. Inf. & Contr., 52:139\u2013158, 1982.","journal-title":"Inf. & Contr."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 997\u2013998. Elsevier\/MIT Press, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"19_CR4","series-title":"number 428 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/3-540-52513-0_2","volume-title":"VDM '90. VDM and Z-Formal Methods in Software Development","author":"J.A. Goguen","year":"1990","unstructured":"J.A. Goguen. An algebraic approach to refinement. In D. Bj\u00d8rner, C.A.R. Hoare, and H. Langmaack, editors, VDM '90. VDM and Z-Formal Methods in Software Development, number 428 in Lect. Notes Comp. Sci., pages 12\u201328. Springer, Berlin, 1990."},{"key":"19_CR5","unstructured":"J.A. Goguen and G. Malcolm. Proof of correctness of object representations. In A.W. Roscoe, editor, A Classical Mind. Essays in honour of C.A.R. Hoare, pages 119\u2013142. Prentice Hall, 1994."},{"key":"19_CR6","unstructured":"J.A. Goguen and G. Malcolm. An extended abstract of a hidden agenda. In J. Meystel, A. Meystel, and R. Quintero, editors, Proceedings of the Conference on Intelligent Systems: A Semiotic Perspective, pages 159\u2013167. Nat. Inst. Stand. & Techn., 1996."},{"key":"19_CR7","series-title":"Lect. Notes Comp. Sci.","volume-title":"Category Theory and Computer Science","author":"U. Hensel","year":"1997","unstructured":"U. Hensel and B. Jacobs. Proof principles for datatypes with iterated recursion. In Category Theory and Computer Science, Lect. Notes Comp. Sci., Springer, Berlin, 1997."},{"key":"19_CR8","series-title":"number 933 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1007\/BFb0022272","volume-title":"Computer Science Logic 1994","author":"C. Hermida","year":"1995","unstructured":"C. Hermida and B. Jacobs. An algebraic view of structural induction. In L. Pacholski and J. Tiuryn, editors, Computer Science Logic 1994, number 933 in Lect. Notes Comp. Sci., pages 412\u2013426. Springer, Berlin, 1995."},{"key":"19_CR9","unstructured":"C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting. Full version of [8], 1996."},{"key":"19_CR10","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"19_CR11","series-title":"number 936 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/3-540-60043-4_57","volume-title":"Algebraic Methods and Software Technology","author":"B. Jacobs","year":"1995","unstructured":"B. Jacobs. Mongruences and cofree coalgebras. In V.S. Alagar and M. Nivat. editors, Algebraic Methods and Software Technology, number 936 in Lect. Notes Comp. Sci., pages 245\u2013260. Springer, Berlin, 1995."},{"key":"19_CR12","series-title":"number 1101 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1007\/BFb0014337","volume-title":"Algebraic Methods and Software Technology","author":"B. Jacobs","year":"1996","unstructured":"B. Jacobs. Coalgebraic specifications and models of deterministic hybrid systems. In M. Wirsing and M. Nivat, editors, Algebraic Methods and Software Technology, number 1101 in Lect. Notes Comp. Sci., pages 520\u2013535. Springer, Berlin, 1996."},{"key":"19_CR13","first-page":"210","volume-title":"number 1098 in Lect. Notes Comp. Sci.","author":"B. Jacobs","year":"1996","unstructured":"B. Jacobs. Inheritance and cofree constructions. In P. Cointe, editor, European Conference on Object-Oriented Programming, number 1098 in Lect. Notes Comp. Sci., pages 210\u2013231. Springer, Berlin, 1996."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"B. Jacobs. Objects and classes, co-algebraically. In B. Freitag, C.B. Jones, C. Lengauer, and H.-J. Schek, editors, Object-Orientation with Parallelism and Persistence, pages 83\u2013103. Kluwer Acad. Publ., 1996.","DOI":"10.1007\/978-1-4613-1437-0_5"},{"key":"19_CR15","series-title":"number 1214 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"787","DOI":"10.1007\/BFb0030641","volume-title":"TAPSOFT'97: Theory and Practice of Software Development","author":"B. Jacobs","year":"1997","unstructured":"B. Jacobs. Behaviour-refinement of coalgebraic specifications with coinductive correctness proofs. In M. Bidoit and M. Dauchet, editors, TAPSOFT'97: Theory and Practice of Software Development, number 1214 in Lect. Notes Comp. Sci., pages 787\u2013802. Springer, Berlin, 1997."},{"key":"19_CR16","first-page":"222","volume":"62","author":"B. Jacobs","year":"1997","unstructured":"B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222\u2013259, 1997.","journal-title":"EATCS Bulletin"},{"issue":"1","key":"19_CR17","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/357195.357202","volume":"5","author":"S. Kamin","year":"1983","unstructured":"S. Kamin. Final data types and their specification. ACM Trans. on Progr. Lang. and Systems, 5(1):97\u2013123, 1983.","journal-title":"ACM Trans. on Progr. Lang. and Systems"},{"key":"19_CR18","series-title":"number 803 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-58043-3_23","volume-title":"A Decade of Concurrency","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. Verification and specification of concurrent programs. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency, number 803 in Lect. Notes Comp. Sci., pages 347\u2013374. Springer, Berlin, 1994."},{"key":"19_CR19","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF01752392","volume":"14","author":"D.J. Lehmann","year":"1981","unstructured":"D.J. Lehmann and M.B. Smyth. Algebraic specification of data types: A synthetic approach. Math. Systems Theory, 14:97\u2013139, 1981.","journal-title":"Math. Systems Theory"},{"key":"19_CR20","volume-title":"Abstraction and Specification in Program Development","author":"B. Liskov","year":"1986","unstructured":"B. Liskov and J. Guttag. Abstraction and Specification in Program Development. The MIT Press, Cambridge, MA, 1986."},{"issue":"2","key":"19_CR21","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N. Lynch","year":"1995","unstructured":"N. Lynch and F. Vaandrager. Forward and backward simulations. I. Untimed systems. Inf. & Comp., 121(2):214\u2013233, 1995.","journal-title":"Inf. & Comp."},{"key":"19_CR22","volume-title":"Texts and Monogr. in Comp. Sci.","author":"E.G. Manes","year":"1986","unstructured":"E.G. Manes and M.A. Arbib. Algebraic Appoaches to Program Semantics. Texts and Monogr. in Comp. Sci., Springer, Berlin, 1986."},{"key":"19_CR23","first-page":"481","volume-title":"Sec. Int. Joint Conf. on Artificial Intelligence","author":"R. Milner","year":"1971","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Sec. Int. Joint Conf. on Artificial Intelligence, pages 481\u2013489. British Comp. Soc. Press, London, 1971."},{"key":"19_CR24","volume-title":"Lect. Notes Comp. Sci.","author":"R. Milner","year":"1989","unstructured":"R. Milner. A Calculus of Communicating Systems. Lect. Notes Comp. Sci. Springer, Berlin, 1989."},{"key":"19_CR25","series-title":"number 1102 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Computer Aided Verification, number 1102 in Lect. Notes Comp. Sci., pages 411\u2013414. Springer, Berlin, 1996."},{"key":"19_CR26","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1017\/S0960129500000694","volume":"5","author":"H. Reichel","year":"1995","unstructured":"H. Reichel. An approach to object semantics based on terminal co-algebras. Math. Struct. in Comp. Sci., 5:129\u2013152, 1995.","journal-title":"Math. Struct. in Comp. Sci."},{"key":"19_CR27","series-title":"number 666 in Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/3-540-56596-5_45","volume-title":"Semantics: Foundations and Applications","author":"J. Rutten","year":"1993","unstructured":"J. Rutten and D. Turi. On the foundations of final semantics: non-standard sets, metric spaces and partial orders. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Semantics: Foundations and Applications, number 666 in Lect. Notes Comp. Sci., pages 477\u2013530. Springer, Berlin, 1993."},{"key":"19_CR28","unstructured":"J.J.M.M. Rutten. Universal coalgebra: a theory of systems. CWI Report CS-R9652, 1996."},{"key":"19_CR29","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1137\/0211062","volume":"11","author":"M.B. Smyth","year":"1982","unstructured":"M.B. Smyth and G.D. Plotkin. The category theoretic solution of recursive domain equations. SIAM Journ. Comput., 11:761\u2013783, 1982.","journal-title":"SIAM Journ. Comput."},{"key":"19_CR30","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0022-0000(79)90011-4","volume":"19","author":"M. Wand","year":"1979","unstructured":"M. Wand. Final algebra semantics and data type extension. Journ. Comp. Syst. Sci, 19:27\u201344, 1979.","journal-title":"Journ. Comp. Syst. Sci"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000477","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T20:40:35Z","timestamp":1549226435000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000477"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540638889","9783540696612"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/bfb0000477","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}