Coalgebras have been proposed as formal basis for the semantics of objects in the sense of object-oriented programming. This paper shows that this semantics provides a smooth interpretation for subtyping, a central notion in object-oriented programming. We show that different characterisations of behavioural subtyping found in the literature can conveniently be expressed in coalgebraic terms. We also investigate the subtle difference between behavioural subtyping and refinement.
@article{ITA_2001__35_1_61_0,
author = {Poll, Erik},
title = {A coalgebraic semantics of subtyping},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
volume = {35},
year = {2001},
pages = {61-81},
mrnumber = {1845875},
zbl = {0990.18004},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2001__35_1_61_0}
}
Poll, Erik. A coalgebraic semantics of subtyping. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 35 (2001) pp. 61-81. http://gdmltest.u-ga.fr/item/ITA_2001__35_1_61_0/
[1] and, A Theory of Objects. Springer, Monogr. Comput. Sci. (1996). | MR 1418635 | Zbl 0876.68014
[2] , Inheritance and Subtyping in a Parallel Object-Oriented Language, in ECOOP'87, edited by J. Bezivin et al.. Springer, Lecture Notes in Comput. Sci. 276 (1987) 232-242.
[3] , Designing an Object-Oriented Languages with Behavioural Subtyping, in Foundations of Object Oriented Languages, edited by J.W. de Bakker et al.. Springer, Lecture Notes in Comput. Sci. 489 (1991) 60-90.
[4] ,, and, On Behavioural Subtyping in LOTOS, in FMOODS'97, Second IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, edited by H. Bowman and J. Derrick. Chapman and Hall (1997) 335-351.
[5] , and, The Hopkins Objects Group (J. Eifrig, S. Smith, V. Trifonov), in On Binary Methods, edited by G.T. Leavens and B.C. Pierce. Theory and Practice of Object Systems 1 (1996) 221-242.
[6] and, On understanding types, data abstraction and polymorphism. Computing Surveys 17 (1985) 471-522.
[7] and, A semantic foundation for specification matching, in Foundations of Component-Based Systems, edited by G.T. Leavens and M. Sitaraman. Cambridge University Press (2000) Chap. 5, 91-109.
[8] , and, Inheritance is not subtyping, in Principles of Programming Languages (POPL). ACM (1990) 125-135.
[9] and, Forcing behavioral subtyping through specification inheritance, in Proc. 18th International Conference on Software Engineering, Berlin, Germany. IEEE (1996) 258-267.
[10] and, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press (1994). | Zbl 0828.68036
[11] ,, and, Reasoning about classes in object-oriented languages: Logical models and tools, in European Symposium on Programming (ESOP), edited by Ch. Hankin. Springer, Lecture Notes in Comput. Sci. 1381 (1998) 105-121. | MR 1697018
[12] , Proof of Correctness of Data Representations. Acta Informatica 1 (1972) 271-281. | Zbl 0244.68009
[13] and, A unifying type-theoretic framework for objects. J. Funct. Programming 5 (1995) 593-635. | MR 1379926
[14] , Invariants, bisimulations and the correctness of coalgebraic refinements, in Algebraic Methodology and Software Technology (AMAST'97), edited by M. Johnson. Springer, Lecture Notes in Comput. Sci. (1997) 276-291.
[15] and, A tutorial on (co)algebras and (co)induction. EATCS Bull. 62 (1997) 222-259. | Zbl 0880.68070
[16] and, A complete algebraic characterization of behavioral subtyping. Acta Informatica 36 (2000) 617-663. | MR 1749285 | Zbl 0951.68018
[17] and, Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32 (1995) 705-778. | MR 1362157 | Zbl 0831.68009
[18] , Data abstraction and hierarchy. SIGPLAN Notices 23 (1988).
[19] and, A behavioral notion of subtyping. TOPLAS 16 (1994) 1811-1841.
[20] , On simulation, subtyping and substitutability in sequential object systems. Formal Aspects of Computing 7 (1995) 620-651. | Zbl 0841.68033
[21] , Object-Oriented Software Construction1997). | Zbl 0987.68516
[22] , Toward a typed foundation for method specialization and inheritance, in Principles of Programming Languages (POPL). ACM (1990) 109-124. | Zbl 0836.68010
[23] and, Simple type-theoretic foundations for object-oriented programming. J. Funct. Programming 4 (1994) 207-247. | Zbl 0817.68052
[24] , Subtyping and Inheritance for Categorical Datatypes, in Theories of Types and Proofs (TTP-Kyoto). Kyoto University Research Insitute for Mathematical Sciences, RIMS Lecture Notes 1023 (1997) 112-125. | MR 1643756 | Zbl 0944.68132
[25] , Behavioural subtyping for a type-theoretic model of objects, in Foundations of Object-Oriented Languages (FOOL5) (1998).
[26] , An approach to object semantics based on terminal co-algebras. Math. Structures Comput. Sci. 5 (1995) 129-152. | MR 1368919 | Zbl 0854.18006
[27] , Universal co-algebra: A theory of systems, CWI Report 9652. CWI (1996). | Zbl 0951.68038
[28] and, Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9 (1997) 229-269. | Zbl 0887.68070
[29] , Encapsulation and inheritance in object-oriented programming languages. ACM SIGPLAN 21 (1986) 38-45. OOPSLA '86 Conference Proceedings, edited by N. Meyrowitz. Portland, Oregon (1986).