Type-preserving compilation of Featherweight Java

ABSTRACT

We present an efficient encoding of core Java constructs in a simple, implementable typed intermediate language. The encoding, after type erasure, has the same operational behavior as a standard implementation using vtables and self-application for method invocation. Classes inherit super-class methods with no overhead. We support mutually recursive classes while preserving separate compilation. Our strategy extends naturally to a significant subset of Java, including interfaces and privacy. The formal translation using Featherweight Java allows comprehensible type-preservation proofs and serves as a starting point for extending the translation to new features. Our work provides a foundation for supporting certifying compilation of Java-like class-based languages in a type-theoretic framework.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: 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]
• 3: Martin Abadi , Marcelo P. Fiore, Syntactic Considerations on Recursive Types, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.242, July 27-30, 1996
• 4: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• 5: Bruce, K. B. 1994. A paradigmatic object-oriented programming language: Design, static typing and semantics. J. Funct. Prog. 4, 2, 127--206.
• 6: 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]
• 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: Cardelli, L. and Leroy, X. 1990. Abstract types and the dot notation. In Proceedings of the IFIP Working Conference on Programming Concepts and Methods. Israel, 466--491.
• 9: Crary, K. 1999. Simple, efficient object encoding using intersection types. Tech. Rep. CMU-CS-99-100, Carnegie Mellon University, Pittsburgh, Pa.
• 10: Karl Crary , Robert Harper , Sidd Puri, What is a recursive module?, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.50-63, May 01-04, 1999, Atlanta, Georgia, United States
• 11: 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]
• 12: 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]
• 13: 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
• 14: Girard, J. Y. 1972. Interpretation fonctionnelle et elimination des coupures dans l'arithmetique d'ordre superieur. Ph.D. dissertation. University of Paris VII, Paris, France.
• 15: Neal Glew, An efficient class and object encoding, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.311-324, October 2000, Minneapolis, Minnesota, United States
• 16: Arthur Neal Glew , Dexter Kozen, Low-level type systems for modularity and object-oriented constructs, 2000
• 17: Healfdene Goguen, Typed Operational Semantics, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, p.186-200, April 10-12, 1995
• 18: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 19: Robert Harper , Christopher Stone, A type-theoretic interpretation of standard ML, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 20: Atsushi Igarashi , Benjamin C. Pierce, On inner classes, Information and Computation, v.177 n.1, p.56-89, 25 August 2002 [doi>10.1006/inco.2002.3092]
• 21: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 22: S. Kamin, Inheritance in smalltalk-80: a denotational definition, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.80-87, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73567]
• 23: Krall, A. and Grafl, R. 1997. CACAO---A 64-bit Java VM Just-In-Time compiler. In Proceedings of the ACM PPoPP'97 Workshop on Java for Science and Engineering Computation. ACM, New York.
• 24: Christopher League , Zhong Shao , Valery Trifonov, Representing Java classes in a typed intermediate language, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.183-196, September 27-29, 1999, Paris, France
• 25: League, C., Trifonov, V., and Shao, Z. 2001a. Functional Java bytecode. In Proceedings of the 5th World Conference on Systemics, Cybernetics, and Informatics. Workshop on Intermediate Representation Engineering for the Java Virtual Machine.
• 26: League, C., Trifonov, V., and Shao, Z. 2001b. Type-preserving compilation of Featherweight Java. In Proceedings of the International Workshop on Foundations of Object-Oriented Languages. (London, England).
• 27: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 28: Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., and Zdancewic, S. 1999a. TALx86: A realistic typed assembly language. In Proceedings of the Workshop on Compiler Support for Systems Software. ACM, New York, 25--35.
• 29: Morrisett, G., Tarditi, D., Cheng, P., Stone, C., Harper, R., and Lee, P. 1996. The TIL/ML compiler: Performance and safety through types. In Proceedings of the Workshop on Compiler Support for Systems Software. ACM, New York.
• 30: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 31: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 32: George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
• 33: Peyton Jones, S. L., Hall, C., Hammond, K., Partain, W., and Wadler, P. 1992. The Glasgow Haskell Compiler: A technical overview. In Proceedings of the UK Joint Framework for Information Technology.
• 34: Pierce, B. C. and Turner, D. N. 1994. Simple type-theoretic foundations for object-oriented programming. J. Funct. Prog. 4, 2 (Apr.), 207--247.
• 35: Proebsting, T. A., Townsend, G., Bridges, P., Hartman, J. H., Newsham, T., and Watterson, S. A. 1997. Toba: Java for applications: A way ahead of time (WAT) compiler. In Proceedings of the 3rd Conference on Object-Oriented Technologies and Systems (COOTS'97).
• 36: Rémy, D. 1993. Syntactic theories and the algebra of record terms. Tech. Rep. 1869, INRIA.
• 37: 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]
• 38: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 39: Shao, Z. 1997. An overview of the FLINT/ML compiler. In Proceedings of the 1997 ACM SIGPLAN Workshop on Types in Compilation. ACM, New York.
• 40: Zhong Shao , Andrew W. Appel, A type-based compiler for standard ML, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.116-129, June 18-21, 1995, La Jolla, California, United States
• 41: 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
• 42: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 43: Vanderwaart, J. C. 1999. Typed intermediate representations for compiling object-oriented languages. Williams College Senior Honors Thesis.
• 44: 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.4 Processors
          Subjects: Compilers

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Object-oriented constructs

General Terms:
Languages, Verification

Keywords:
Java, object encodings, type systems, typed intermediate languages