{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:29Z","timestamp":1761611069030},"reference-count":31,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":6163,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1996,9]]},"DOI":"10.1016\/0304-3975(96)00039-4","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T00:48:18Z","timestamp":1027644498000},"page":"3-55","source":"Crossref","is-referenced-by-count":49,"title":["Behavioural theories and the proof of behavioural properties"],"prefix":"10.1016","volume":"165","author":[{"given":"Michel","family":"Bidoit","sequence":"first","affiliation":[]},{"given":"Rolf","family":"Hennicker","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(96)00039-4_BIB1","series-title":"Proc. DISCO'93","first-page":"2","article-title":"Proving the correctness of algebraic implementations by the ISAR system","volume":"Vol. 722","author":"Bauer","year":"1993"},{"key":"10.1016\/0304-3975(96)00039-4_BIB2","series-title":"Proc. AMAST'91","first-page":"216","article-title":"Proving the correctness of algebraically specified software: modularity and observability issues","author":"Bernot","year":"1992"},{"key":"10.1016\/0304-3975(96)00039-4_BIB3","series-title":"Proc. First Internat. Workshop on Larch","first-page":"18","article-title":"How to prove observational theorems with LP","author":"Bidoit","year":"1993"},{"key":"10.1016\/0304-3975(96)00039-4_BIB4","series-title":"Proc. ALP'94","first-page":"41","article-title":"Proving behavioural theorems with standard first-order logic","volume":"Vol. 850","author":"Bidoit","year":"1994"},{"key":"10.1016\/0304-3975(96)00039-4_BIB5","series-title":"Recent Trends in Data Type Specification","first-page":"153","article-title":"Behavioural theories","volume":"Vol. 906","author":"Bidoit","year":"1995"},{"key":"10.1016\/0304-3975(96)00039-4_BIB6_1","series-title":"Modular correctness proofs of behavioural implementations","author":"Bidoit","year":"1995"},{"key":"10.1016\/0304-3975(96)00039-4_BIB6_2","series-title":"Proc. of AMAST'95","first-page":"152","article-title":"Proving the correctness of behavioural implementations","volume":"Vol.936","author":"Bidoit","year":"1995"},{"issue":"2\u20133","key":"10.1016\/0304-3975(96)00039-4_BIB7_1","article-title":"Behavioural and abstractor specifications","volume":"25","author":"Bidoit","year":"1995","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(96)00039-4_BIB7_2","series-title":"Proc. of ESOP'94","first-page":"105","article-title":"Characterizing behavioural semantics and abstractor semantics","volume":"Vol. 788","author":"Bidoit","year":"1994"},{"key":"10.1016\/0304-3975(96)00039-4_BIB8","series-title":"Proc. CAAP'96","first-page":"241","article-title":"Behavioural satisfaction and equivalence in concrete model categories","volume":"Vol. 1059","author":"Bidoit","year":"1996"},{"key":"10.1016\/0304-3975(96)00039-4_BIB9","article-title":"Fundamentals of Algebraic Specification 1. Equations and initial semantics","volume":"Vol. 6","author":"Ehrig","year":"1985"},{"key":"10.1016\/0304-3975(96)00039-4_BIB10","article-title":"Fundamentals of Algebraic Specification 2","volume":"Vol. 21","author":"Ehrig","year":"1990"},{"key":"10.1016\/0304-3975(96)00039-4_BIB11","series-title":"Proc. Third internat. Conf. on Rewriting Techniques and Applications","first-page":"137","article-title":"An overview of LP, the Larch Prover","volume":"Vol. 355","author":"Garland","year":"1989"},{"key":"10.1016\/0304-3975(96)00039-4_BIB12","series-title":"Proc. 9th ICALP","first-page":"265","article-title":"Universal realization, persistent interconnection and implementation of abstract modules","volume":"Vol. 140","author":"Goguen","year":"1982"},{"issue":"4","key":"10.1016\/0304-3975(96)00039-4_BIB13","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/BF01642507","article-title":"Context induction: a proof principle for behavioural abstractions and algebraic implementations","volume":"3","author":"Hennicker","year":"1991","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/0304-3975(96)00039-4_BIB14","doi-asserted-by":"crossref","unstructured":"R. Hennicker, M. Wirsing and M. Bidoit, Proof systems for structured specifications with observability operators, Theoret. Comput. Sci., to appear.","DOI":"10.1016\/S0304-3975(96)00162-4"},{"key":"10.1016\/0304-3975(96)00039-4_BIB15","series-title":"Proc. TAPSOFT'95","first-page":"247","article-title":"On behavioural abstraction and behavioural satisfaction in higher-order logic","volume":"Vol. 915","author":"Hofmann","year":"1995"},{"key":"10.1016\/0304-3975(96)00039-4_BIB16","series-title":"El\u00e9ments de Logique Math\u00e9matique","author":"Kreisel","year":"1967"},{"key":"10.1016\/0304-3975(96)00039-4_BIB17","article-title":"Proving correctness of refinement and implementation","author":"Malcolm","year":"1994"},{"key":"10.1016\/0304-3975(96)00039-4_BIB18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","article-title":"Fully abstract models of typed \u03bb-calculi","volume":"4","author":"Milner","year":"1977","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(96)00039-4_BIB19","series-title":"Recent Trends in Data Type Specification","first-page":"184","article-title":"Initial behaviour semantics for algebraic specification","volume":"Vol. 332","author":"Nivela","year":"1988"},{"key":"10.1016\/0304-3975(96)00039-4_BIB20","series-title":"Recent Trends in Data Type Specification","first-page":"93","article-title":"Implementation and behavioural equivalence: A survey","volume":"Vol. 655","author":"Orejas","year":"1993"},{"key":"10.1016\/0304-3975(96)00039-4_BIB21","series-title":"Proc. IFIP Working Conference, The Role of Abstract Models in Information Processing","article-title":"Initial restrictions of behaviour","author":"Reichel","year":"1985"},{"key":"10.1016\/0304-3975(96)00039-4_BIB22","doi-asserted-by":"crossref","DOI":"10.1515\/9783112573426","article-title":"Initial computability, algebraic specifications, and partial algebras","author":"Reichel","year":"1987"},{"key":"10.1016\/0304-3975(96)00039-4_BIB23","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":"J. Comput. System Sci."},{"key":"10.1016\/0304-3975(96)00039-4_BIB24","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF00283329","article-title":"Toward formal development of programs from algebraic specification: implementation revisited","volume":"25","author":"Sannella","year":"1988","journal-title":"Acta inform."},{"key":"10.1016\/0304-3975(96)00039-4_BIB25","series-title":"Proc. FCT'83","first-page":"413","article-title":"A kernel language for algebraic specifications and implementation","volume":"Vol. 158","author":"Sannella","year":"1983"},{"key":"10.1016\/0304-3975(96)00039-4_BIB26","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0167-6423(90)90057-K","article-title":"Behavioural correctness of data representation","volume":"14","author":"Schoett","year":"1990","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(96)00039-4_BIB27","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1145\/69622.357192","article-title":"Data type specification: parameterization and the power of specification techniques","volume":"4","author":"Thatcher","year":"1982","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"10.1016\/0304-3975(96)00039-4_BIB28","doi-asserted-by":"crossref","DOI":"10.1016\/B978-0-444-88074-1.50018-4","article-title":"Algebraic specification","author":"Wirsing","year":"1990"},{"key":"10.1016\/0304-3975(96)00039-4_BIB29","series-title":"Logic and Algebra of Specification, International Summer School Marktoberdorf, 1991","article-title":"Structured Specifications: Syntax, Semantics and Proof Calculus","author":"Wirsing","year":"1993"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397596000394?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397596000394?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T01:48:51Z","timestamp":1681609731000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397596000394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["0304397596000394"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(96)00039-4","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}