Christopher League
Zhong Shao
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.
- 1.M. Abadi, L. Cardelli, and R. Viswanathan. An interpretation of objects and object types. In Prec. 23rd ACM SIGPL,4N-SIGACT Syrnp. on Principles of Programming Languages (POPL'96), pages 396-- 409, St. Petersburg, January 1996. ACM Press. Google Scholar
Digital Library
- 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.Google ScholarCross Ref
- 3.N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to Java bytecodes. In Prec. lnt 'I Conf. on Functional Programming (ICFP'98), pages 129-140. Google ScholarDigital Library
- 4.K. Bruce, L. Cardelli, G. Castagna, The Hopkins Objects Group, G. T. Leavens, and B. Pierce. On binary methods. Theory and Practice of Object Systems, 1(3):221-242, December 1995. Google ScholarDigital Library
- 5.K. Bruce, L. Cardelli, and B. Pierce. Comparing object encodings. Information and Computation (to appear), 1998. Google ScholarDigital Library
- 6.K. B. Bruce. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 4(2), 1994.Google ScholarCross Ref
- 7.P. Canning, W. Cook, W. Hill, J. Mitchell, and W. Olthoff. F-bounded polyrnorphism for object-oriented programming. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture, pages 273-280, 1989. Google ScholarDigital Library
- 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.Google Scholar
- 9.L. Cardelli and G. Longo. A semantic basis for Quest. Journal of Functional Programming, 1 (4), 1991.Google ScholarCross Ref
- 10.J. Dean, G. DeFouw, D. Grove, V. Litvinov, and C. Chambers. Vortex: An optimizing compiler for object-oriented languages. In Prec. ACM SIGPLAN Conf. on Object-Oriented Programming Systems, Languages, and Apptications (OOPSLA '96), pages 83-100, San Jose, October 1996. ACM. Google ScholarDigital Library
- 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.Google Scholar
- 12.S. Drossopoulou and S. Eisenbach, Towards an operational semantics and proof of type soundness for Java, April 1998.Google Scholar
- 13.J. Eifrig, S. Smith, V. Trifonov, and A. Zwarico. An interpretation of typed OOP in a language with state. Lisp and Symbolic Computation, 8(4):357-397, 1995. Google ScholarDigital Library
- 14.K. Fisher. Type Systems for Object-Oriented Programming Languages. PhD thesis, Stanford University, August 1996. Google ScholarDigital Library
- 15.K. Fisher and J. Mitchell. On the relationship between classes, objects and data abstraction. 7heo~ and Practice of Object Systems (to appear), 1998. Google ScholarDigital Library
- 16.K. Fisher and J, Reppy. The design of a class mechanism for Moby, In Prec. ACM SIGPLAN '99 Co~ on Pros. Lang. Design and tmple. mentation, pages 37-49, New York, May 1999. ACM Press. Google ScholarDigital Library
- 17.M. Flatt, S. Krishtaamurthi, and M. Felleisen. A programmer's reduction semantics for classes and mixins. Technical Report 97-293, Rice University, 1997.Google Scholar
- 18.J.Y. Girard. Interpretation Fonctionnelle et Elimination des Coupures clans l',4rithmetique d'Ordre ~uperieur. Phi) thesis, University of Paris VII, 1972.Google Scholar
- 19.N. Glewo Type dispatch for named hierarchical types. In Prec. 1999 ACM SIGPLAN International Conference on Functional Programming (ICFP '99). ACM Press, September 1999. Google ScholarDigital Library
- 20.N. Heintze and 3. G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Prvc. 2.5th ,4CMSIGPLAN:SIGACTSymp. on Principles of Programming Languages (POPL'98), pages 365-377. Google ScholarDigital Library
- 21.M. Hofmann and B. Pierce. A unifying type-theoretic framework for objects. Journal of Functional .Programming, January 1994.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 24.X. Leroy and E Rouaix. Security properties of typed applets. In Prec. 25th ACM SIGPLAN-SIGACT Syrup. on Principles of Programming Languages (POPL '98), pages 391403. Google ScholarDigital Library
- 25.T. Lindholm and E Yellin. The Java Virtual Machine Specification (Second Edition). Addison-Wesley, 1999. Google ScholarDigital Library
- 26.MicrosoR Win32 VM for Java object model, 1998.Google Scholar
- 27.M. Odersky and P. Wadler. Pizza into Java: Translating theory inw practice. In Prec. 24th ACM SiGPLAN-SIGACT Syrup. on Principles of Programming Languages (POPL '97), pages 146-159. Google ScholarDigital Library
- 28.J. Palsberg and P. Orba~k, Trust in the X-calculu:~. Journal of Functional Programming, 7(6):557-591, November 1997. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 31.D. R~my. Syntactic theories and the algebra of nx:ord terms. Technical Report 1869, INRIA, 1993.Google Scholar
- 32.D. R6my and 1. VouiUon. Objective ML: A simple object-oriented extension of ML. In Prec. 24th ,4CM SIGPLAN-SIG,4CT Syrup. on Principles of Programming Languages (POPL'97), pages 40-53. Google ScholarDigital Library
- 33.J.C. Reynolds. Towards a theory of type structure. In Prec., Colloque sur la Programmation, Lecture Notes in Computer Science, volume 19, pages 408-425. Springer- Verlag, Berlin, 1974. Google ScholarDigital Library
- 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.Google Scholar
- 35.Z. Shoo. Typed common intermediate format. In Prec. USENIX Conf. on Domain-Specific Languages, pages 89-101, Santa Barbara, CA, October 1997. Google ScholarDigital Library
- 36.Z. Shao. Typed cross-module compilation. In Prec. Int 7 Conf. on Functional Programming (ICFP'98), pages 141-152. Google ScholarDigital Library
- 37.Z. Shao, C. League, and S. Mormier. Implementing typed intermediate languages. In Prec. Int'l Conf. on Functional Programming (ICFP '98), pages 313-323. Google ScholarDigital Library
- 38.A. Wright, S. Jagannathan, C. Ungureanu, and A. Hertzma~. Compiling Java to a typed lambda-calculus: A preliminary report. In Proc. Second Int 7 Workshop on Types in Compilation (TIC'98), pages 1-14, Kyoto, March 1998. Google ScholarDigital Library
Index Terms
- Representing Java classes in a typed intermediate language
Recommendations
Representing Java classes in a typed intermediate language
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, ...
Implementing typed intermediate languages
Recent advances in compiler technology have demonstrated the benefits of using strongly typed intermediate languages to compile richly typed source languages (e.g., ML). A type-preserving compiler can use types to guide advanced optimizations and to ...
A simple typed intermediate language for object-oriented languages
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesTraditional class and object encodings are difficult to use in practical type-preserving compilers because of the complexity of the encodings. We propose a simple typed intermediate language for compiling object-oriented languages and prove its ...
Comments