Atsushi Igarashi
Benjamin C. Pierce
Philip Wadler
Abstract
Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.
- ABADI,M.AND CARDELLI, L. 1996. A Theory of Objects. Springer Verlag, New York, NY.]] Google Scholar
- AGESEN, O., FREUND,S.N.,AND MITCHELL, J. C. 1997. Adding type parameterization to the Java language. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'97). SIGPLAN Not. 32, 10. ACM Press, Atlanta, GA, 49-65.]] Google Scholar
- ANCONA,D.AND ZUCCA, E. 2001. True modules for Java-like languages. In Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP2001), J. L. Knudsen, Ed. Lecture Notes in Computer Science. Springer-Verlag, Budapest, Hungary.]] Google Scholar
- BARENDREGT, H. P. 1984. The Lambda Calculus, revised ed. North Holland, Amsterdam, The Netherlands.]]Google Scholar
- BONO,V.AND FISHER, K. 1998. An imperative first-order calculus with object extension. In Proceedings of the 12th European Conference on Object-Oriented Programming (ECOOP'98), E. Jul, Ed. LNCS 1445. Springer Verlag, 462-497.]] Google Scholar
- BONO, V., PATEL,A.J.,AND SHMATIKOV, V. 1999a. A core calculus of classes and mixins. In Proceedings of the 13th European Conference on Object-Oriented Programming (ECOOP'99). LNCS 1628. Springer Verlag, 43-66.]] Google Scholar
- BONO, V., PATEL,A.J.,SHMATIKOV,V.,AND MITCHELL, J. C. 1999b. A core calculus of classes and objects. In Proceedings of the 15th Conference on the Mathematical Foundations of Programming Semantics (MFPS XV). Elsevier. Available through http://www.elsevier.nl/locate/entcs/ volume20.html.]]Google Scholar
- BRACHA, G., ODERSKY, M., STOUTAMIRE,D.,AND WADLER, P. 1998. Making the future safe for the past: Adding genericity to the Java programming language. In Proceedings of the ACMSIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'98), C. Chambers, Ed. ACM Press, New York, NY, 183-200.]] Google Scholar
- BRUCE, K. B. 1994. A paradigmatic object-oriented programming language: Design, static typing and semantics. J. Funct. Program. 4, 2 (April), 127-206.]]Google Scholar
- CARDELLI, L., MARTINI, S., MITCHELL,J.C.,AND SCEDROV, A. 1994. An extension of system F with subtyping. Inf. Comput. 109, 1-2, 4-56.]] Google Scholar
- CARTWRIGHT,R.AND STEELE JR., G. L. 1998. Compatible genericity with run-time types for the Java programming language. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'98), C. Chambers, Ed. ACM Press, New York, NY, 201-215.]] Google Scholar
- DROSSOPOULOU, S., EISENBACH,S.,AND KHURSHID, S. 1999. Is the Java type system sound? Theory Pract. Object Syst. 7, 1, 3-24.]] Google Scholar
- DUGGAN, D. 1999. Modular type-based reverse engineering of parameterized types in Java code. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), L. M. Northrop, Ed. ACM Press, New York, NY, 97-113.]] Google Scholar
- FELLEISEN,M.AND FRIEDMAN, D. P. 1998. A Little Java, A Few Patterns. MIT Press, Cambridge, MA.]] Google Scholar
- FISHER,K.AND MITCHELL, J. C. 1998. On the relationship between classes, objects, and data abstraction. Theory Pract. Object Syst. 4, 1, 3-25.]] Google Scholar
- FLATT, M., KRISHNAMURTHI,S.,AND FELLEISEN, M. 1998a . Classes and mixins. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 171-183.]] Google Scholar
- FLATT, M., KRISHNAMURTHI,S.,AND FELLEISEN, M. 1998b. A programmer's reduction semantics for classes and mixins. Tech. Rep. TR97-293, Computer Science Dept., Rice University. Feb. Corrected version in June, 1999.]]Google Scholar
- IGARASHI,A.AND PIERCE, B. C. 2000. On inner classes. In Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP2000), E. Bertino, Ed. LNCS 1850. Springer Verlag, 129-153. Extended version to appear in Inf. Comput.]] Google Scholar
- IGARASHI, A., PIERCE,B.C.,AND WADLER, P. 2001. A recipe for raw types. In Informal Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages (FOOL8). London, UK. Available through http://www.cs.williams.edu/kim/FOOL/FOOL8.html.]]Google Scholar
- LEAGUE, C., TRIFONOV,V.,AND SHAO, Z. 2001. Type-preserving compilation of Featherweight Java. In Informal Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages (FOOL8). London, UK. Available through http://www.cs.williams.edu/kim/FOOL/ FOOL8.html.]]Google Scholar
- MYERS,A.C.,BANK,J.A.,AND LISKOV, B. 1997. Parameterized types for Java. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 132-145.]] Google Scholar
- NIPKOW,T.AND VON OHEIMB, D. 1998. Java light is type-safe- definitely. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 161-170.]] Google Scholar
- ODERSKY,M.AND WADLER, P. 1997. Pizza into Java: Translating theory into practice. In Proceedings of the ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 146-159.]] Google Scholar
- PIERCE, B. C. 2002. Types and Programming Languages. MIT Press, Cambridge, MA.]] Google Scholar
- PIERCE,B.C.AND TURNER, D. N. 1994. Simple type-theoretic foundations for object-oriented programming. J. Funct. Program. 4, 2 (April), 207-247.]]Google Scholar
- SCHULTZ, U. 2001. Partial evaluation for class-based object-oriented languages. In Proceedings of the 2nd Symposium on Programs as Data Objects (PADO II), O. Danvy and A. Filinski, Eds. LNCS 2053. Springer Verlag, 173-197.]] Google Scholar
- STUDER, T. 2000. Constructive foundations for Featherweight Java. Available through http:// iamwww.unibe.ch/tstuder/.]]Google Scholar
- SYME, D. 1997. Proving Java type soundness. Tech. Rep. 427, Computer Lab. Univ. of Cambridge. June.]]Google Scholar
- VIROLI,M.AND NATALI, A. 2000. Parametric polymorphism in Java: an approach to translation based on reflective features. In Proceedings of the ACMSIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'00), D. Lea, Ed. ACM Press, New York, NY, 146-165.]] Google Scholar
- WAND, M. 1989. Type inference for objects with instance variables and inheritance. Tech. Rep. NU-CCS-89-2, College of Computer Science, Northeastern Univ. Feb.]]Google Scholar
- WRIGHT,A.K.AND FELLEISEN, M. 1994. A syntactic approach to type soundness. Inf. Comput. 115, 1 (Nov.), 38-94.]] Google Scholar
Index Terms
- Featherweight Java: a minimal core calculus for Java and GJ
Recommendations
Featherweight Java: a minimal core calculus for Java and GJ
Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step ...
Variant parametric types: A flexible subtyping scheme for generics
We develop the mechanism of variant parametric types as a means to enhance synergy between parametric and inclusion polymorphism in object-oriented programming languages. Variant parametric types are used to control both the subtyping between different ...
Featherweight Java: a minimal core calculus for Java and GJ
OOPSLA '99: Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applicationsSeveral recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step ...
Comments