|
 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.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
|
 |
2
|
Ole Agesen , Stephen N. Freund , John C. Mitchell, Adding type parameterization to the Java language, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.49-65, October 05-09, 1997, Atlanta, Georgia, United States
|
| |
3
|
|
| |
4
|
BARENDREGT, H. P. 1984. The Lambda Calculus, revised ed. North Holland, Amsterdam, The Netherlands.
|
| |
5
|
|
| |
6
|
|
| |
7
|
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.
|
| |
8
|
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
|
| |
9
|
BRUCE, K. B. 1994. A paradigmatic object-oriented programming language: Design, static typing and semantics. J. Funct. Program. 4, 2 (April), 127-206.
|
| |
10
|
|
| |
11
|
Robert Cartwright , Guy L. Steele, Jr., Compatible genericity with run-time types for the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.201-215, October 18-22, 1998, Vancouver, British Columbia, Canada
|
| |
12
|
|
| |
13
|
Dominic Duggan, Modular type-based reverse engineering of parameterized types in Java code, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.97-113, November 01-05, 1999, Denver, Colorado, United States
|
| |
14
|
|
| |
15
|
|
| |
16
|
Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 19-21, 1998, San Diego, California, United States
[doi> 10.1145/268946.268961]
|
| |
17
|
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.
|
| |
18
|
|
| |
19
|
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.
|
| |
20
|
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.
|
| |
21
|
|
| |
22
|
|
| |
23
|
|
| |
24
|
|
| |
25
|
PIERCE,B.C.AND TURNER, D. N. 1994. Simple type-theoretic foundations for object-oriented programming. J. Funct. Program. 4, 2 (April), 207-247.
|
| |
26
|
|
| |
27
|
STUDER, T. 2000. Constructive foundations for Featherweight Java. Available through http:// iamwww.unibe.ch/tstuder/.
|
| |
28
|
SYME, D. 1997. Proving Java type soundness. Tech. Rep. 427, Computer Lab. Univ. of Cambridge. June.
|
| |
29
|
Mirko Viroli , Antonio Natali, Parametric polymorphism in Java: an approach to translation based on reflective features, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.146-165, October 2000, Minneapolis, Minnesota, United States
|
| |
30
|
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.
|
| |
31
|
|
CITED BY 85
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Alex Potanin , James Noble , Robert Biddle, Generic ownership: practical ownership control in programming languages, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Vijay S. Menon , Neal Glew , Brian R. Murphy , Andrew McCreight , Tatiana Shpeisman , Ali-Reza Adl-Tabatabai , Leaf Petersen, A verifiable SSA program representation for aggressive compiler optimization, ACM SIGPLAN Notices, v.41 n.1, p.397-408, January 2006
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Chris Andreae , Yvonne Coady , Celina Gibbs , James Noble , Jan Vitek , Tian Zhao, Scoped types and aspects for real-time Java memory management, Real-Time Systems, v.37 n.1, p.1-44, October 2007
|
|
|
|
|
|
|
|
|
|
|
|
Yoav Zibin , Alex Potanin , Mahmood Ali , Shay Artzi , Adam Kie|un , Michael D. Ernst, Object and reference immutability using Java generics, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Tian Zhao , Jason Baker , James Hunt , James Noble , Jan Vitek, Implicit ownership types for memory management, Science of Computer Programming, v.71 n.3, p.213-241, May, 2008
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Shay Artzi , Adam Kieżun , Jaime Quinonez , Michael D. Ernst, Parameter reference immutability: formal definition, inference tool, and comparison, Automated Software Engineering, v.16 n.1, p.145-192, March 2009
|
|
|
|
|
|
Sara Capecchi , Mario Coppo , Mariangiola Dezani-Ciancaglini , Sophia Drossopoulou , Elena Giachino, Amalgamating sessions and methods in object-oriented languages with generics, Theoretical Computer Science, v.410 n.2-3, p.142-167, February, 2009
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.3