An interpretation of extensible objects

  • Gérard Boudol
  • Silvano Dal-Zilio
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)


We provide a translation of Fisher-Honsell-Mitchell’s delegation-based object calculus with subtyping into a λ-calculus with extensible records.The target type system is an extension of the system \( \mathcal{F}^\omega \) of types depending on types with recursion,extensible records and a form of bounded universal quantification.We show that our translation is computationally adequate,that the typing rules of Fisher-Honsell-Mitchell’s calculus can be derived in a rather simple and natural way,and that our system enjoys the standard subject reduction property.


Type System Typing Rule Typing Context Method Invocation Lambda Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi, Baby Modula-3 and a theory of objects, J. of Functional Programming Vol 4, No 2 (1994) 249–283.zbMATHGoogle Scholar
  2. 2.
    M. Abadi, L. Cardelli, A theory of primitive objects: untyped and first-order systems, TACS’ 94, Lecture Notes in Comput. Sci. 789 (1994) 296–320.Google Scholar
  3. 3.
    M. Abadi, L. Cardelli, R. Viswanathan, An interpretation of objects and object types, POPL’ 96 (1996) 396–409.Google Scholar
  4. 4.
    V. Bono, L. Liquori, A subtyping for the Fisher-Honsell-Mitchell lambda calculus of objects, CSL’ 94, Lecture Notes in Comput. Sci. 933 (1994) 16–30.Google Scholar
  5. 5.
    V. Bono, M. Bugliesi, Matching constraints for the lambda calculus of objects, TLCA’ 97, Lecture Notes in Comput. Sci. 1210 (1997) 46–63.Google Scholar
  6. 6.
    K. Bruce, The equivalence of two semantic definitions for inheritance in object-oriented languages, MFPS’ 92, Lecture Notes in Comput. Sci. 598 (1992) 102–124.Google Scholar
  7. 7.
    K. Bruce, L. Cardelli, B. Pierce, Comparing object encodings, TACS’ 97, Lecture Notes in Comput. Sci. 1281 (1997) 415–438.Google Scholar
  8. 8.
    K. Bruce, L. Petersen, A. Fiech, Subtyping is not a good “match” for object-oriented languages, ECOOP’ 97, Lecture Notes in Comput. Sci. 1241 (1997) 104–127.Google Scholar
  9. 9.
    L. Cardelli, A semantics of multiple inheritance, Semantics of Data Types, Lecture Notes in Comput. Sci. 173 (1984) 51–67. Also published in Information and Computation, Vol 76 (1988).Google Scholar
  10. 10.
    L. Cardelli, P. Wegner, On understanding types, data abstraction, and polymorphism, Computing Surveys 17 (1985) 471–522.CrossRefGoogle Scholar
  11. 11.
    A. Compagnoni, Subject reduction and minimal types for higher order subtyping, Tech. Rep. ECS-LFCS-97-363, University of Edinburgh (1997).Google Scholar
  12. 12.
    W. Cook, W. Hill, P. Canning, Inheritance is not subtyping, POPL’ 90 (1990) 125–135.Google Scholar
  13. 13.
    K. Fisher, F. Honsell, J. Mitchell, A lambda calculus of objects and method specialization, LICS’ 93 (1993) 26–38.Google Scholar
  14. 14.
    K. Fisher, J. Mitchell, Notes on typed object-oriented programming, TACS’ 94, Lecture Notes in Comput. Sci. 789 (1994) 844–885.Google Scholar
  15. 15.
    K. Fisher, J. Mitchell, A delegation-based object calculus with subtyping, FCT’ 95, Lecture Notes in Comput. Sci. 965 (1995) 42–61.Google Scholar
  16. 16.
    K. Fisher, Types Systems for Object-Oriented Programming Languages, PhD Thesis, Stanford University (1996).Google Scholar
  17. 17.
    P. Di Gianantonio, F. Honsell, L. Liquori, A lambda-calculus of objects with self-inficted extension, OOPSLA’ 98, ACM SIGPLAN Notices Vol 33, No 10 (1998) 166–178.CrossRefGoogle Scholar
  18. 18.
    J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur, Thèse d’Ètat, Université Paris 7 (1972).Google Scholar
  19. 19.
    M. Hofmann, B. Pierce, A unifying type-theoretic framework for objects, J. of Functional Programming Vol. 5, No 4 (1995) 593–635.MathSciNetCrossRefGoogle Scholar
  20. 20.
    J. Mitchell, Toward a typed foundation for method specialization and inheritance, POPL’ 90 (1990) 109–124.Google Scholar
  21. 21.
    R. Viswanathan, Full abstraction for first-order objects with recursive types and subtyping, LICS’ 98 (1998).Google Scholar
  22. 22.
    M. Wand, Complete type inference for simple objects, LICS’ 87 (1987) 37–44.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Gérard Boudol
    • 1
  • Silvano Dal-Zilio
    • 1
  1. 1.INRIA Sophia AntipolisSophia Antipolis CedexFrance

Personalised recommendations