A Coalgebraic Semantics of Subtyping

Erik Poll

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 35, Issue: 1, page 61-81
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Poll, Erik. "A Coalgebraic Semantics of Subtyping." RAIRO - Theoretical Informatics and Applications 35.1 (2010): 61-81. <http://eudml.org/doc/221987>.

@article{Poll2010,
abstract = { 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. },
author = {Poll, Erik},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {coalgebras; object-oriented programming; subtyping; refinement},
language = {eng},
month = {3},
number = {1},
pages = {61-81},
publisher = {EDP Sciences},
title = {A Coalgebraic Semantics of Subtyping},
url = {http://eudml.org/doc/221987},
volume = {35},
year = {2010},
}

TY - JOUR
AU - Poll, Erik
TI - A Coalgebraic Semantics of Subtyping
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 35
IS - 1
SP - 61
EP - 81
AB - 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.
LA - eng
KW - coalgebras; object-oriented programming; subtyping; refinement
UR - http://eudml.org/doc/221987
ER -

References

top
  1. M. Abadi and L. Cardelli, A Theory of Objects. Springer, Monogr. Comput. Sci. (1996).  Zbl0876.68014
  2. P. America, 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. P. America, 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. H. Bowman, C. Briscoe-Smith, J. Derrick and B. Strulo, 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. K.B. Bruce, L. Cardelli and G. Castagna, 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 Systems1 (1996) 221-242.  
  6. L. Cardelli and P. Wegner, On understanding types, data abstraction and polymorphism. Computing Surveys17 (1985) 471-522.  
  7. Y. Chen and B.H.C. Cheng, 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. W.R. Cook, W.L. Hill and P.S. Canning, Inheritance is not subtyping, in Principles of Programming Languages (POPL). ACM (1990) 125-135.  Zbl0837.68061
  9. K.K. Dhara and G.T. Leavens, Forcing behavioral subtyping through specification inheritance, in Proc. 18th International Conference on Software Engineering, Berlin, Germany. IEEE (1996) 258-267.  
  10. C.A. Gunter and J.C. Mitchell, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press (1994).  Zbl0828.68036
  11. 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 (ESOP), edited by Ch. Hankin. Springer, Lecture Notes in Comput. Sci. 1381 (1998) 105-121.  
  12. C.A.R. Hoare, Proof of Correctness of Data Representations. Acta Informatica1 (1972) 271-281.  Zbl0244.68009
  13. M. Hofmann and B.C. Pierce, A unifying type-theoretic framework for objects. J. Funct. Programming5 (1995) 593-635.  
  14. B. Jacobs, 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. B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. EATCS Bull.62 (1997) 222-259.  Zbl0880.68070
  16. G.T. Leavens and D. Pigozzi, A complete algebraic characterization of behavioral subtyping. Acta Informatica36 (2000) 617-663.  Zbl0951.68018
  17. G.T. Leavens and W.E. Weihl, Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica32 (1995) 705-778.  Zbl0831.68009
  18. B.H. Liskov, Data abstraction and hierarchy. SIGPLAN Notices 23 (1988).  
  19. B.H. Liskov and J.M. Wing, A behavioral notion of subtyping. TOPLAS16 (1994) 1811-1841.  
  20. I. Maung, On simulation, subtyping and substitutability in sequential object systems. Formal Aspects of Computing7 (1995) 620-651.  Zbl0841.68033
  21. B. Meyer, Object-Oriented Software Construction. Prentice Hall, 2nd Rev. Edition (1997).  Zbl0987.68516
  22. J.C. Mitchell, Toward a typed foundation for method specialization and inheritance, in Principles of Programming Languages (POPL). ACM (1990) 109-124.  
  23. B.C. Pierce and D.N. Turner, Simple type-theoretic foundations for object-oriented programming. J. Funct. Programming4 (1994) 207-247.  Zbl0817.68052
  24. E. Poll, 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.  
  25. E. Poll, Behavioural subtyping for a type-theoretic model of objects, in Foundations of Object-Oriented Languages (FOOL5) (1998).  
  26. H. Reichel, An approach to object semantics based on terminal co-algebras. Math. Structures Comput. Sci.5 (1995) 129-152.  Zbl0854.18006
  27. J. Rutten, Universal co-algebra: A theory of systems, CWI Report 9652. CWI (1996).  
  28. D. Sannella and A. Tarlecki, Essential concepts of algebraic specification and program development. Formal Aspects of Computing9 (1997) 229-269.  Zbl0887.68070
  29. A. Snyder, Encapsulation and inheritance in object-oriented programming languages. ACM SIGPLAN21 (1986) 38-45. OOPSLA '86 Conference Proceedings, edited by N. Meyrowitz. Portland, Oregon (1986).  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.