Coalgebras for binary methods : properties of bisimulations and invariants
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 35 (2001) no. 1, pp. 83-111.

Coalgebras for endofunctors 𝒞𝒞 can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors 𝒞 op ×𝒞𝒞. This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many standard results.

Classification : 03E20,  03G30,  68Q55,  68Q65
Mots clés : binary method, coalgebra, bisimulation, invariant, object-orientation
@article{ITA_2001__35_1_83_0,
     author = {Tews, Hendrik},
     title = {Coalgebras for binary methods : properties of bisimulations and invariants},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {83--111},
     publisher = {EDP-Sciences},
     volume = {35},
     number = {1},
     year = {2001},
     zbl = {0983.68126},
     mrnumber = {1845876},
     language = {en},
     url = {http://www.numdam.org/item/ITA_2001__35_1_83_0/}
}
TY  - JOUR
AU  - Tews, Hendrik
TI  - Coalgebras for binary methods : properties of bisimulations and invariants
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2001
DA  - 2001///
SP  - 83
EP  - 111
VL  - 35
IS  - 1
PB  - EDP-Sciences
UR  - http://www.numdam.org/item/ITA_2001__35_1_83_0/
UR  - https://zbmath.org/?q=an%3A0983.68126
UR  - https://www.ams.org/mathscinet-getitem?mr=1845876
LA  - en
ID  - ITA_2001__35_1_83_0
ER  - 
Tews, Hendrik. Coalgebras for binary methods : properties of bisimulations and invariants. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 35 (2001) no. 1, pp. 83-111. http://www.numdam.org/item/ITA_2001__35_1_83_0/

[1] P. Aczel and P.F. Mendler, A final coalgebra theorem, in Proc. of the Conference on Category Theory and Computer Science, edited by D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts and A. Poigné. Springer, Lecture Notes in Comput. Sci. 389 (1989) 357-365. | MR 1031572

[2] H.P. Barendregt, Lambda calculi with types, edited by S. Abramsky, D.M. Gabbay and T.S.E. Maibaum. Oxford Science Publications, Handb. Log. Comput. Sci. 2 (1992). | MR 1381697

[3] K. Bruce, L. Cardelli and G. Castagna, The Hopkins Object Group, edited by G.T. Leavens and B. Pierce, On binary methods. Theory and Practice of Object Systems 1 (1995) 221-242.

[4] C. Cîrstea, A coalgebraic equational approach to specifying observational structures, in Coalgebraic Methods in Computer Science '99, edited by B. Jacobs and J. Rutten. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 19 (1999). | Zbl 1002.68095

[5] J. Goguen and G. Malcolm, A hidden agenda. Theoret. Comput. Sci. 245 (2000) 55-101. | MR 1784537 | Zbl 0946.68070

[6] J. Gosling, B. Joy and G. Steele, The Java Language Specification. Addison-Wesley (1996). | Zbl 0865.68001

[7] R. Hennicker and A. Kurz, (Ω,Ξ)-Logic: On the algebraic extension of coalgebraic specifications, in Coalgebraic Methods in Computer Science '99, edited by B. Jacobs and J. Rutten. Elsevier, Electron. Notes Theor. Comput. Sci. 19 (1999) 195-212. | Zbl 0918.68064

[8] U. Hensel, Definition and Proof Principles for Data and Processes, Ph.D. Thesis. University of Dresden, Germany (1999).

[9] U. Hensel, M. Huisman, B. Jacobs and H. Tews, Reasoning about classes in object-oriented languages: Logical models and tools, in European Symposium on Programming, edited by Ch. Hankin. Springer, Berlin, Lecture Notes in Comput. Sci. 1381 (1998) 105-121.

[10] C. Hermida and B. Jacobs, Structural induction and coinduction in a fibrational setting. Inform. and Comput. (1998) 107-152. | MR 1641597 | Zbl 0941.18006

[11] B. Jacobs, Objects and classes, co-algebraically, in Object-Orientation with Parallelism and Peristence, edited by B. Freitag, C.B. Jones, C. Lengauer and H.-J. Schek. Kluwer Acad. Publ. (1996) 83-103.

[12] B. Jacobs, Invariants, bisimulations and the correctness of coalgebraic refinements, in Algebraic Methodology and Software Technology, edited by M. Johnson. Springer, Berlin, Lecture Notes in Comput. Sci. 1349 (1997) 276-291.

[13] B. Jacobs, Categorical Logic and Type Theory. North Holland, Elsevier, Stud. Logic Found. Math. 141 (1999). | MR 1674451 | Zbl 0911.03001

[14] B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. EATCS Bull. 62 (1997) 222-259. | Zbl 0880.68070

[15] Y. Kawahara and M. Mori, A small final coalgebra theorem. Theoret. Comput. Sci. 233 (2000) 129-145. | MR 1732181 | Zbl 0952.68101

[16] X. Leroy, D. Doligez, J. Garrigue, D. Rémy and J. Vouillon, The Objective Caml system, release 3.01, March 2001. Available at URL http://caml.inria.fr/ocaml/htmlman/.

[17] B. Meyer, Eiffel: The Language. Prentice Hall (1992). | Zbl 0779.68013

[18] R. Milner, Communication and Concurrency. Prentice Hall (1989). | Zbl 0683.68008

[19] S. Owre, S. Rajan, J.M. Rushby, N. Shankar and M. Srivas, PVS: Combining specification, proof checking, and model checking, in Computer Aided Verification, edited by R. Alur and T.A. Henzinger. Springer, Berlin, Lecture Notes in Comput. Sci. 1102 (1996) 411-414.

[20] E. Poll and J. Zwanenburg, From algebras and coalgebras to dialgebras, in Coalgebraic Methods in Computer Science '01, edited by A. Corradini, M. Lenisa and U. Montanari. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 44 (2001).

[21] H. Reichel, Behavioural validity of conditional equations in abstract data types, in Contributions to General Algebra 3. Teubne, (1985); in Proc. of the Vienna Conference (June 21-24, 1984). | MR 815137 | Zbl 0616.68020

[22] H. Reichel, An approach to object semantics based on terminal co-algebras. Math. Structure Comput. Sci. 5 (1995) 129-152. | MR 1368919 | Zbl 0854.18006

[23] G. Roşu, Hidden Logic, Ph.D. Thesis. University of California at San Diego (2000).

[24] J. Rothe, H. Tews and B. Jacobs, The coalgebraic class specification language CCSL. J. Universal Comput. Sci. 7 (2001) 175-193. | MR 1829826 | Zbl 0970.68104

[25] J.J.M.M. Rutten, Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249 (2000) 3-80. | MR 1791953 | Zbl 0951.68038

[26] B. Stroustrup, The C++ Programming Language: Third Edition. Addison-Wesley Publishing Co., Reading, Mass. (1997). | Zbl 0609.68011

[27] H. Tews, Coalgebras for binary methods, in Coalgebraic Methods in Computer Science '00, edited by H. Reichel. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 33 (2000). | Zbl 0966.68049