Representing Java classes in a typed intermediate language

ABSTRACT

We propose a conservative extension of the polymorphic lambda calculus (F^ω) as an intermediate language for compiling languages with name-based class and interface hierarchies. Our extension enriches standard F^ω with recursive types, existential types, and row polymorphism, but only ordered records with no subtyping. Basing our language on F^ω makes it also a suitable target for translation from other higher-order languages; this enables the safe interoperation between class-based and higher-order languages and the reuse of common type-directed optimization techniques, compiler back ends, and runtime support.We present the formal semantics of our intermediate language and illustrate its features by providing a formal translation from a subset of Java, including classes, interfaces, and private instance variables. The translation preserves the name-based hierarchical relation between Java classes and interfaces, and allows access to private instance variables of parameters of the same class as the one defining the method. It also exposes the details of method invocation and instance variable access and allows many standard optimizations to be performed on the object-oriented code.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Ramesh Viswanathan, An interpretation of objects and object types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.396-409, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237809]
• 2: A. W. Appel and D. B. MacQueen. Standard ML of New Jersey. Technical Report CS-TR~329-91, Princeton University Department of Computer Science, June 1991.
• 3: Nick Benton , Andrew Kennedy , George Russell, Compiling standard ML to Java bytecodes, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.129-140, September 26-29, 1998, Baltimore, Maryland, United States
• 4: Kim Bruce , Luca Cardelli , Giuseppe Castagna , Gary T. Leavens , Benjamin Pierce, On binary methods, Theory and Practice of Object Systems, v.1 n.3, p.221-242, Fall 1995
• 5: Kim B. Bruce , Luca Cardelli , Benjamin C. Pierce, Comparing object encodings, Information and Computation, v.155 n.1-2, p.108-133, Nov./Dec. 1999 [doi>10.1006/inco.1999.2829]
• 6: K. B. Bruce. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 4(2), 1994.
• 7: Peter Canning , William Cook , Walter Hill , Walter Olthoff , John C. Mitchell, F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.273-280, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99392]
• 8: L. Cardelli and X. Leroy. Abstract types and the dot notation. In Prec. IFIP Working Conf. on Programming Concepts and Methods, pages 46649 I, Israel, April 1990.
• 9: L. Cardelli and G. Longo. A semantic basis for Quest. Journal of Functional Programming, 1 (4), 1991.
• 10: Jeffrey Dean , Greg DeFouw , David Grove , Vassily Litvinov , Craig Chambers, Vortex: an optimizing compiler for object-oriented languages, Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.83-100, October 06-10, 1996, San Jose, California, United States
• 11: S. Drossopoulou and S. Eisenbach. Java is type safe---probably. In Prec. I I th European Conf. on Object-Oriented Programming, Febru~ ary 1997.
• 12: S. Drossopoulou and S. Eisenbach, Towards an operational semantics and proof of type soundness for Java, April 1998.
• 13: Jonathan Eifrig , Scott Smith , Valery Trifonov , Amy Zwarico, An interpretation of typed OOP in a language, Lisp and Symbolic Computation, v.8 n.4, p.357-397, Dec. 1995 [doi>10.1007/BF01018829]
• 14: Kathleen Shanahan Fisher , John C. Mitchell, Type systems for object-oriented programming languages, 1996
• 15: Kathleen Fisher , John C. Mitchell, On the relationship between classes, objects, and data abstraction, Theory and Practice of Object Systems, v.4 n.1, p.3-25, 1998 [doi>10.1002/(SICI)1096-9942(1998)4:1<3::AID-TAPO2>3.3.CO;2-2]
• 16: Kathleen Fisher , John Reppy, The design of a class mechanism for Moby, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.37-49, May 01-04, 1999, Atlanta, Georgia, United States
• 17: M. Flatt, S. Krishtaamurthi, and M. Felleisen. A programmer's reduction semantics for classes and mixins. Technical Report 97-293, Rice University, 1997.
• 18: J.Y. Girard. Interpretation Fonctionnelle et Elimination des Coupures clans l',4rithmetique d'Ordre ~uperieur. Phi) thesis, University of Paris VII, 1972.
• 19: Neal Glew, Type dispatch for named hierarchical types, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.172-182, September 27-29, 1999, Paris, France
• 20: Nevin Heintze , Jon G. Riecke, The SLam calculus: programming with secrecy and integrity, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.365-377, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268976]
• 21: M. Hofmann and B. Pierce. A unifying type-theoretic framework for objects. Journal of Functional .Programming, January 1994.
• 22: A. Krall and R. Graft. CACAO---a 64~bit Java VM Just-In-Time compiler. In Prec. ACM PPoPP'97 Workshop on Java .{br Science and Engineering Computation., 1997.
• 23: C. League, Z. Shao, and V. Trifonov. Representing Java classes in a typed intermediate language (extended version). Technical Report YALEU/DCS/RR- 1180, Department of Computer Science, Yale University, New Haven, CT, June ! 999.
• 24: Xavier Leroy , François Rouaix, Security properties of typed applets, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.391-403, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268979]
• 25: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 26: MicrosoR Win32 VM for Java object model, 1998.
• 27: Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
• 28: P. Ørbæk , J. Palsberg, Trust in the λ-calculus, Journal of Functional Programming, v.7 n.6, p.557-591, November 1997 [doi>10.1017/S0956796897002906]
• 29: B. C. Pierce and D. N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207-247, April 1994.
• 30: T. A. Proebsting, G. Townsend, P. Bridges, J. H. Hartman, T. Nowsham, and S. A. Watterson. Toba: Java for applications: A way ahead of time (WAT) compiler. In Prec. Third Conf. on Object-Oriented Technologies and Systems (C00TS'97), 1997.
• 31: D. R~my. Syntactic theories and the algebra of nx:ord terms. Technical Report 1869, INRIA, 1993.
• 32: Didier Rémy , Jérôme Vouillon, Objective ML: a simple object-oriented extension of ML, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-53, January 15-17, 1997, Paris, France [doi>10.1145/263699.263707]
• 33: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 34: Z. Shoo. An overview of the FLINT/ML compiler. In Prec. First Int'l Workshop on 73pes in Compilation (TIC'97), Amsterdam, June 1997.
• 35: Z. Shoo. Typed common intermediate format. In Prec. USENIX Conf. on Domain-Specific Languages, pages 89-101, Santa Barbara, CA, October 1997.
• 36: Zhong Shao, Typed cross-module compilation, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.141-152, September 26-29, 1998, Baltimore, Maryland, United States
• 37: Zhong Shao , Christopher League , Stefan Monnier, Implementing typed intermediate languages, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.313-323, September 26-29, 1998, Baltimore, Maryland, United States
• 38: Andrew K. Wright , Suresh Jagannathan , Cristian Ungureanu , Aaron Hertzmann, Compiling Java to a Typed Lambda-Calculus: A Preliminary Report, Proceedings of the Second International Workshop on Types in Compilation, p.9-27, March 25-27, 1998

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Theory