Skip to main content
Springer Nature Link
Log in

A unifying type-theoretic framework for objects

  • Conference paper
  • First Online:
STACS 94 (STACS 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 775))

Included in the following conference series:

Abstract

We give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, objects, methods, message passing, and subtyping, by introducing an explicit Object type constructor and suitable introduction, elimination, and equality rules. The resulting abstract framework provides a common basis for justifying and comparing previous encodings of objects based on recursive record types [7, 9], F-bounded quantification [4, 13, 19], and existential types [23].

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Martín Abadi. Doing without F-bounded quantification. Message to Types electronic mail list, February 1992.

    Google Scholar 

  2. Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. In Proceedings of the Eighteenth ACM Symposium on Principles of Programming Languages, pages 104–118, Orlando, FL, January 1991. Also available as DEC Systems Research Center Research Report number 62, August 1990. To appear in TOPLAS.

    Google Scholar 

  3. S. Bainbridge, P. Freyd, A. Scedrov, and P. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35–64, 1990.

    Google Scholar 

  4. Kim B. Bruce. Safe type checking in a statically typed object-oriented programming language. In Proceedings of the Twentieth ACM Symposium on Principles of Programming Languages, 1993. To appear in Journal of Functional Programming.

    Google Scholar 

  5. Kim Bruce and John Mitchell. PER models of subtyping, recursive types and higher-order polymorphism. In Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages, Albequerque, NM, January 1992.

    Google Scholar 

  6. Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John Mitchell. F-bounded quantification for object-oriented programming. In Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 273–280, September 1989.

    Google Scholar 

  7. Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988. Preliminary version in Semantics of Data Types, Kahn, MacQueen, and Plotkin, eds., Springer-Verlag LNCS 173, 1984.

    Google Scholar 

  8. Luca Cardelli. Notes about 0261–01. Unpublished notes, October 1990.

    Google Scholar 

  9. Luca Cardelli. Extensible records in a pure calculus of subtyping. Research report 81, DEC Systems Research Center, January 1992. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (The MIT Press; to appear, 1993).

    Google Scholar 

  10. Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of system F with subtyping. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software (Sendai, Japan), number 526 in Lecture Notes in Computer Science, pages 750–770. Springer-Verlag, September 1991.

    Google Scholar 

  11. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), December 1985.

    Google Scholar 

  12. G. Castagna, G. Ghelli, and G. Longo. A calculus for overloaded functions with subtyping. In ACM conference on LISP and Functional Programming, pages 182–192, San Francisco, July 1992. ACM Press. Also available as Rapport de Recherche LIENS-92-4, Ecole Normale Supérieure, Paris.

    Google Scholar 

  13. William R. Cook, Walter L. Hill, and Peter S. Canning. Inheritance is not subtyping. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 125–135, San Francisco, CA, January 1990. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (The MIT Press; to appear, 1993).

    Google Scholar 

  14. O. J. Dahl and K. Nygaard. SIMULA—An ALGOL-based simulation language. Communications of the ACM, 9(9):671–678, September 1966.

    Google Scholar 

  15. Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, 1972.

    Google Scholar 

  16. Adele Goldberg and David Robson. Smalltalk-80: The Language and Its Implementation. Addison-Wesley, Reading, MA, 1983.

    Google Scholar 

  17. Martin Hofmann and Benjamin Pierce. An abstract view of objects and subtyping (preliminary report). Technical Report ECS-LFCS-92-226, University of Edinburgh, LFCS, 1992.

    Google Scholar 

  18. A. Kock. Strong functors and monoidal monads. Various Publications Series 11, Aarhus Universitet, 1970.

    Google Scholar 

  19. John C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pages 109–124, January 1990. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (The MIT Press; to appear, 1993).

    Google Scholar 

  20. John C. Mitchell. A type-inference approach to reduction properties and semantics of polymorphic expressions. In Gérard Huet, editor, Logical Foundations of Functional Programming, University of Texas at Austin Year of Programming Series, pages 195–212. Addison-Wesley, 1990.

    Google Scholar 

  21. John Mitchell and Gordon Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3), July 1988.

    Google Scholar 

  22. Benjamin C. Pierce and Robert Pollack. Higher-order subtyping. Unpublished manuscript, August 1992.

    Google Scholar 

  23. Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 1993. To appear; a preliminary version appeared in Principles of Programming Languages, 1993, and as University of Edinburgh technical report ECS-LFCS-92-225, under the title “Object-Oriented Programming Without Recursive Types”.

    Google Scholar 

  24. Benjamin C. Pierce and David N. Turner. Statically typed friendly functions via partially abstract types. Technical Report ECS-LFCS-93-256, University of Edinburgh, LFCS, April 1993. Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899.

    Google Scholar 

  25. John Reynolds. Towards a theory of type structure. In Proc. Collogue sur la Programmation, pages 408–425, New York, 1974. Springer-Verlag LNCS 19.

    Google Scholar 

  26. John C. Reynolds. User defined types and procedural data structures as complementary approaches to data abstraction. In David Gries, editor, Programming Methodology, A Collection of Articles by IFIP WG2.3, pages 309–317. Springer-Verlag, New York, 1978. Reprinted from S. A. Schuman (ed.), New Advances in Algorithmic Languages 1975, Inst. de Recherche d'Informatique et d'Automatique, Rocquencourt, 1975, pages 157–168. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (The MIT Press; to appear, 1993).

    Google Scholar 

  27. Gavin C. Wraith. A note on categorical datatypes. Number 389 in Lecture Notes in Computer Science. Springer-Verlag, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Edinburgh, The King's Buildings, EH9 3JZ, Edinburgh, UK

    Martin Hofmann & Benjamin Pierce

Authors
  1. Martin Hofmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benjamin Pierce
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Patrice Enjalbert Ernst W. Mayr Klaus W. Wagner

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hofmann, M., Pierce, B. (1994). A unifying type-theoretic framework for objects. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds) STACS 94. STACS 1994. Lecture Notes in Computer Science, vol 775. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57785-8_146

Download citation

  • DOI: https://doi.org/10.1007/3-540-57785-8_146

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57785-0

  • Online ISBN: 978-3-540-48332-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation