{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,29]],"date-time":"2023-04-29T12:10:43Z","timestamp":1682770243395},"reference-count":41,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3681,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,7]]},"DOI":"10.1016\/s1571-0661(04)80645-5","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"285-302","source":"Crossref","is-referenced-by-count":0,"title":["Inductive Behavioral Proofs by Unhiding"],"prefix":"10.1016","volume":"82","author":[{"given":"Grigore","family":"Ro\u015fu","sequence":"first","affiliation":[]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB1","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1145\/77600.77621","article-title":"Module algebra","volume":"37","author":"Bergstra","year":"1990","journal-title":"Journal of the ACM"},{"issue":"6","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB2","doi-asserted-by":"crossref","first-page":"1194","DOI":"10.1145\/227683.227687","article-title":"Equational specifications, complete rewriting systems, and computable and semicomputable algebras","volume":"42","author":"Bergstra","year":"1995","journal-title":"Journal of the ACM"},{"issue":"1-2","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB3","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0304-3975(94)00017-D","article-title":"Observational specifications and the indistinguishability assumption","volume":"139","author":"Bernot","year":"1995","journal-title":"TCS"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB4","doi-asserted-by":"crossref","unstructured":"N. Berregeb, A. Bouhoula, and M. Rusinowitch. Observational proofs with critical contexts. In Proceedings of FASE'98, volume 1382 of LNCS. 1998.","DOI":"10.1007\/BFb0053582"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB5","series-title":"Algebraic and Logic Programming (ALP'94) volume 850 of LNCS","first-page":"41","article-title":"Proving behavioural theorems with standart first-order logic","author":"Bidoit","year":"1994"},{"issue":"1","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(96)00039-4","article-title":"Behavioral theories and the proof of behavioral properties","volume":"165","author":"Bidoit","year":"1996","journal-title":"Theoretical Computer Science"},{"issue":"11","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB7","doi-asserted-by":"crossref","first-page":"951","DOI":"10.1007\/s002360050149","article-title":"Modular correctness proofs of behavioural implementations","volume":"35","author":"Bidoit","year":"1998","journal-title":"Acta Informatica"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB8","series-title":"OBJ\/CafeOBJ\/Maude at FM'99","first-page":"83","article-title":"Observer complete definitions are behaviourally coherent","author":"Bidoit","year":"1999"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB9","series-title":"A Classical Mind: Essays in Honour of C.A.R. Hoare","first-page":"75","article-title":"Hiding and behaviour: an institutional approach","author":"Burstall","year":"1994"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB10","doi-asserted-by":"crossref","unstructured":"S. Buss and G. Ro\u015fu. Incompleteness of behavioral logics. In Proceeding of CMCS'00, volume 33 of ENTCS, pages 61\u201379. Elsevier, 2000.","DOI":"10.1016\/S1571-0661(05)80756-X"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB11","series-title":"Recent Trends in Algebraic Development Techniques volume 1589 of LNCS","article-title":"Semantic constructions for hidden algebra","author":"Ci\u00eerstea","year":"1999"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB12","doi-asserted-by":"crossref","unstructured":"M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In Proceedings of WRLA, volume 4 of ENTCS. Elsevier, 1996.","DOI":"10.1016\/S1571-0661(04)00034-9"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB13","doi-asserted-by":"crossref","unstructured":"R. Diaconescu and K. Futatsugi. CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. World Scientific, 1998. AMAST Series in Computing, volume 6.","DOI":"10.1142\/3831"},{"issue":"1","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB14","first-page":"74","article-title":"Behavioral coherence in object-oriented algebraic specification","volume":"6","author":"Diaconescu","year":"2000","journal-title":"J. of Universal Computer Science"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB15","series-title":"Logical Environments","first-page":"83","article-title":"Logical support for modularization","author":"Diaconescu","year":"1993"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB16","doi-asserted-by":"crossref","unstructured":"V. Giarrantana, F. Gimona, and U. Montanari. Observability concepts in abstract data specifications. In Proceedings of MFCS, vol. 45 of LNCS. 1976.","DOI":"10.1007\/3-540-07854-1_231"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB17","series-title":"Topology and Category Theory in Computer Science","first-page":"357","article-title":"Types as theories","author":"Goguen","year":"1991"},{"issue":"1","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB18","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","article-title":"Institutions: Abstract model theory for specification and programming","volume":"39","author":"Goguen","year":"1992","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB19","doi-asserted-by":"crossref","unstructured":"J. Goguen and R. Diaconescu. Towards an algebraic semantics for the object paradigm. In Proceedings of WADT, volume 785 of LNCS. Springer, 1994.","DOI":"10.1007\/3-540-57867-6_1"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB20","doi-asserted-by":"crossref","unstructured":"J. Goguen, K. Lin, and G. Ro\u015fu. Circular coinductive rewriting. In Proceedings of Automated Software Engineering 2000, pages 123\u2013131. IEEE, 2000.","DOI":"10.1109\/ASE.2000.873657"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB21","doi-asserted-by":"crossref","unstructured":"J. Goguen, K. Lin, and G. Ro\u015fu. Behavioral and coinductive rewriting. In Proceedings of WRLA'01, volume 36 of ENTCS, pages 1\u201322. Elsevier, 2001.","DOI":"10.1016\/S1571-0661(05)80128-8"},{"issue":"3","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB22","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S0960129599002777","article-title":"Hidden coinduction: Behavioral correctness proofs for objects","volume":"9","author":"Goguen","year":"1999","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB23","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/S0304-3975(99)00275-3","article-title":"A hidden agenda","volume":"245","author":"Goguen","year":"2000","journal-title":"TCS"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB24","doi-asserted-by":"crossref","unstructured":"J. Goguen and J. Meseguer. Universal realization, persistent interconnection and implementation of abstract modules. In Proceedings of ICALP, volume 140 of LNCS, pages 265\u2013281. Springer, 1982.","DOI":"10.1007\/BFb0012775"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB25","doi-asserted-by":"crossref","unstructured":"J. Goguen and G. Ro\u015fu. Hiding more of hidden algebra. In Proceeding of FM'99, volume 1709 of LNCS, pages 1704\u20131719. Springer, 1999.","DOI":"10.1007\/3-540-48118-4_40"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB26","series-title":"Software Engineering with OBJ: algebraic specification in action","first-page":"3","article-title":"Introducing OBJ","author":"Goguen","year":"2000"},{"issue":"4","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB27","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/BF01642507","article-title":"Context induction: a proof principle for behavioral abstractions","volume":"3","author":"Hennicker","year":"1991","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB28","doi-asserted-by":"crossref","unstructured":"R. Hennicker and M. Bidoit. Observational logic. In Proceedings of AMAST'98, volume 1548 of LNCS, pages 263\u2013277. Springer, 1999.","DOI":"10.1007\/3-540-49253-4_20"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB29","first-page":"222","article-title":"A tutorial on (co)algebras and (co)induction","volume":"62","author":"Jacobs","year":"1997","journal-title":"Bulletin of the European Association for Theoretical Comp. Science"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB30","doi-asserted-by":"crossref","unstructured":"D. Lucanu, O. Gheorghie\u015f, and A. Apetrei. Bisimulation and hidden algebra. In Proceedings of CMCS'99, volume 19 of ENTCS, pages 213\u2013232. 1999.","DOI":"10.1016\/S1571-0661(05)80276-2"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB31","first-page":"37","article-title":"Limits of the algebraic specification of abstract data types","author":"Majster","year":"1977","journal-title":"SIGPLAN Notices"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB32","series-title":"Algebraic Methods in Semantics","first-page":"459","article-title":"Initiality, induction and computability","author":"Meseguer","year":"1985"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB33","unstructured":"S. Mikami. Semantics of equational specifications with module import and verification method of behavioral equations. In Proceedings of CafeOBJ Symposium. Japan Advanced Institute for Science and Technology, 1998."},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB34","doi-asserted-by":"crossref","unstructured":"P. Padawitz. Towards the one-tiered design of data types and transition systems. In Proceedings of WADT'97, volume 1376 of LNCS, pages 365\u2013380. Springer, 1998.","DOI":"10.1007\/3-540-64299-4_45"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB35","first-page":"339","article-title":"Information distribution aspects of design methodlogy","volume":"71","author":"Parnas","year":"1972","journal-title":"Information Processing"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB36","unstructured":"H. Reichel. Behavioural equivalence \ue4f8 a unifying concept for initial and final specifications. In Proceedings of the 3rd Hungarian Computer Science Conference. Akademiai Kiado, 1981."},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB37","series-title":"Contributions to General Algebra 3","article-title":"Behavioural validity of conditional equations in abstract data types","author":"Reichel","year":"1985"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB38","unstructured":"G. Ro\u015fu. Hidden Logic. PhD thesis, University of California at San Diego, 2000."},{"issue":"1-2","key":"10.1016\/S1571-0661(04)80645-5_NEWBIB39","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/S0304-3975(00)00129-8","article-title":"Equational axiomatizability for coalgebra","volume":"260","author":"Ro\u015fu","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB40","series-title":"Automated Deduction in Classical and Non-Classical Logics volume 1761 of LNAI","article-title":"Hidden congruent deduction","author":"Ro\u015fu","year":"2000"},{"key":"10.1016\/S1571-0661(04)80645-5_NEWBIB41","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1016\/0022-0000(87)90023-7","article-title":"On observational equivalence and algebraic specification","volume":"34","author":"Sannella","year":"1987","journal-title":"Journal of Computer and System Science"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806455?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806455?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,4,29]],"date-time":"2023-04-29T11:42:10Z","timestamp":1682768530000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104806455"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["S1571066104806455"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80645-5","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}