Skip to main content
SpringerLink
Log in

A Nominal Theory of Objects with Dependent Types

  • Conference paper
ECOOP 2003 – Object-Oriented Programming (ECOOP 2003)

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

Included in the following conference series:

Abstract

We design and study vObj, a calculus and dependent type system for objects and classes which can have types as members. Type members can be aliases, abstract types, or new types. The type system can model the essential concepts of JAVA’s inner classes as well as virtual types and family polymorphism found in BETA or GBETA. It can also model most concepts of SML-style module systems, including sharing constraints and higher-order functors, but excluding applicative functors. The type system can thus be used as a basis for unifying concepts that so far existed in parallel in advanced object systems and in module systems. The paper presents results on confluence of the calculus, soundness of the type system, and undecidability of type checking.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  2. Ancona, D., Zucca, E.: A primitive calculus for module systems. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Ancona, D., Zucca, E.: A calculus of module systems. Journal of Functional Programming (2002)

    Google Scholar 

  4. Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic 48(4), 931–940 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  5. Bono, V., Patel, A., Shmatikov, V.: A core calculus of classes and mixins. In: Proceedings of the 13th European Conference on Object-Oriented Programming, Lisbon, Portugal, pp. 43–66 (1999)

    Google Scholar 

  6. Boudol, G.: The recursive record semantics of objects revisited. Technical Report 4199, INRIA (June 2001); To appear in Journal of Functional Programming

    Google Scholar 

  7. Bracha, G.: The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance. PhD thesis, University of Utah (1992)

    Google Scholar 

  8. Bracha, G., Griswold, D.: Extending Smalltalk with mixins. In: OOPSLA 1996 Workshop on Extending the Smalltalk Language (April 1996)

    Google Scholar 

  9. Bracha, G., Lindstrom, G.: Modularity meets inheritance. In: Proceedings of the IEEE Computer Society International Conference on Computer Languages, Washington, DC, pp. 282–290. IEEE Computer Society, Los Alamitos (1992)

    Chapter  Google Scholar 

  10. Bruce, K.B.: Foundations of Object-Oriented Programming Languages: Types and Semantics. MIT Press, Cambridge (2002) ISBN 0-201-17888-5

    Google Scholar 

  11. Bruce, K.B., Fiech, A., Petersen, L.: Subtyping is not a good “Match” for object-oriented languages. In: Proceedings of the European Conference on Object-Oriented Programming, pp. 104–127 (1997)

    Google Scholar 

  12. Bruce, K.B., Odersky, M., Wadler, P.: A statical safe alternative to virtual types. In: Proceedings of the 5th International Workshop on Foundations of Object-Oriented Languages, San Diego, USA (1998)

    Google Scholar 

  13. Cardelli, L., Donahue, J., Glassman, L., Jordan, M., Kalsow, B., Nelson, G.: Modula-3 language definition. ACM SIGPLAN Notices 27(8), 15–42 (1992)

    Article  Google Scholar 

  14. Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of system F with subtyping. Information and Computation 109(1-2), 4–56 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  15. Cardelli, L., Mitchell, J.: Operations on records. Mathematical Structures in Computer Science 1, 3–38 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  16. Crary, K., Harper, R., Puri, S.: What is a recursive module? In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 50–63 (1999)

    Google Scholar 

  17. Dahl, O.-J., Myhrhaug, B., Nygaard, K.: Simula: Common base language. Technical report, Norwegian Computing Center (October 1970)

    Google Scholar 

  18. Duggan, D., Sourelis, C.: Mixin modules. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming, Philadelphia, Pennsylvania, June 1996, pp. 262–273 (1996)

    Google Scholar 

  19. Ernst, E.: gBeta: A language with virtual attributes, block structure and propagating, dynamic inheritance. PhD thesis, Department of Computer Science, University of Aarhus, Denmark (1999)

    Google Scholar 

  20. Ernst, E.: Family polymorphism. In: Proceedings of the European Conference on Object-Oriented Programming, Budapest, Hungary, pp. 303–326 (2001)

    Google Scholar 

  21. Flatt, M., Krishnamurthi, S., Felleisen, M.: Classes and mixins. In: Proceedings of the 25th ACM Symposium on Principles of Programming Languages, San Diego, California, pp. 171–183 (1998)

    Google Scholar 

  22. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification. Java Series, 2nd edn., Sun Microsystems (2000) ISBN 0-201-31008-2

    Google Scholar 

  23. Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: Proceedings of the 21st ACM Symposium on Principles of Programming Languages (January 1994)

    Google Scholar 

  24. Igarashi, A.: On inner classes. In: Proceedings of the European Conference on Object-Oriented Programming, Cannes, France (June 2000)

    Google Scholar 

  25. Igarashi, A., Pierce, B.C.: Foundations for virtual types. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, p. 161. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  26. Igarashi, A., Pierce, B.C.: Foundations for virtual types. Information and Computation 175(1), 34–49 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  27. Igarishi, A., Pierce, B., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. In: Proc. OOPSLA (November 1999)

    Google Scholar 

  28. Leroy, X.: A syntactic theory of type generativity and sharing. In: ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon (1994)

    Google Scholar 

  29. MacQueen, D.: Modules for Standard ML. In: Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, New York, August 1984, pp. 198–207 (1984)

    Google Scholar 

  30. Lehrmann Madsen, O., Møller-Pedersen, B., Nygaard, K.: Object-Oriented Programming in the BETA Programming Language. Addison-Wesley, Reading (1993) ISBN 0-201-62430-3

    Google Scholar 

  31. Madsen, O.L., Møller-Pedersen, B.: Virtual Classes: A powerful mechanism for object-oriented programming. In: Proceedings OOPSLA 1989, October 1989, pp. 397–406 (1989)

    Google Scholar 

  32. Nipkow, T., von Oheimb, D.: Java-light is type-safe — definitely. In: Cardelli, L. (ed.) Conference Record of the 25th Symposium on Principles of Programming Languages (POPL 1998), San Diego, California, pp. 161–170. ACM Press, New York (1998)

    Google Scholar 

  33. Odersky, M.: Report on the programming language Scala, École Polytechnique Fédérale de Lausanne, Switzerland (2002), http://lamp.epfl.ch/odersky/scala @

  34. Odersky, M., Cremet, V., Röckl, C., Zenger, M.: A nominal theory of objects with dependent types. Technical report IC/2002/70, EPFL, Switzerland (September 2002), http://lamp.epfl.ch/papers/technto.pdf @; Odersky, M., Cremet, V., Röckl, C., Zenger, M.: A nominal theory of objects with dependent types. In: Proc. FOOL 10 (January 2003), http://www.cis.upenn.edu/~bcpierce/FOOL/FOOL10.html

  35. Ostermann, K.: Dynamically composable collaborations with delegation layers. In: Proceedings of the 16th European Conference on Object-Oriented Programming, Málaga, Spain (2002)

    Google Scholar 

  36. Russo, C.: First-class structures for Standard ML. In: Proceedings of the 9th European Symposium on Programming, Berlin, Germany, pp. 336–350 (2000)

    Google Scholar 

  37. Smaragdakis, Y., Batory, D.: Implementing layered designs with mixin layers. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, p. 550. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  38. Thorup, K.K.: Genericity in Java with virtual types. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 444–471. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  39. Thorup, K.K., Torgersen, M.: Unifying genericity: Combining the benefits of virtual types and parameterized classes. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, p. 186. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  40. Torgersen, M.: Virtual types are statically safe. In: 5th Workshop on Foundations of Object-Oriented Languages, San Diego, CA, USA (January 1998)

    Google Scholar 

  41. Torgersen, M.: Inheritance is specialization. In: The Inheritance Workshop with ECOOP 2002 (June 2002), http://www.cs.auc.dk/eernst/inhws/ @; Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115 (1994)

  42. Zenger, M.: Type-safe prototype-based component evolution. In: Proceedings of the European Conference on Object-Oriented Programming, Mälaga, Spain (June 2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École Polytechnique Fédérale de Lausanne , INR Ecublens, 1015, Lausanne, Switzerland

    Martin Odersky, Vincent Cremet, Christine Röckl & Matthias Zenger

Authors
  1. Martin Odersky
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vincent Cremet
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christine Röckl
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Matthias Zenger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research,  

    Luca Cardelli

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Odersky, M., Cremet, V., Röckl, C., Zenger, M. (2003). A Nominal Theory of Objects with Dependent Types. In: Cardelli, L. (eds) ECOOP 2003 – Object-Oriented Programming. ECOOP 2003. Lecture Notes in Computer Science, vol 2743. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45070-2_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45070-2_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40531-3

  • Online ISBN: 978-3-540-45070-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation