[Prev][Next][Index][Thread]

New paper: Featherweight Java, a Core Calculus for Java and GJ

We are pleased to announce the availability of a new paper formalizing
key features of the type system of GJ, an extension of Java with
parametric classes and methods.  The full paper is available as:

     http://www.yl.is.s.u-tokyo.ac.jp/~igarashi/papers/fj-techrep.ps.gz
     http://www.cis.upenn.edu/~bcpierce/papers/fj-tr.ps.gz

A shorter and more readable version (without proofs), which will be
presented at OOPSLA '99 next week, is also available:

     http://www.yl.is.s.u-tokyo.ac.jp/~igarashi/papers/fj-oopsla.ps.gz
     http://www.cis.upenn.edu/~bcpierce/papers/fj-oopsla.ps.gz
                                
Regards,

	Atsushi Igarashi
	Benjamin Pierce
	Philip Wadler

------------------------------------------------------------------------

     	Featherweight Java: A Core Calculus for Java and GJ

	Atsushi Igarashi, Benjamin Pierce, and 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 full 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 syntax, type
rules, and operational semantics of Featherweight Java fit on one
page, making it easier to understand 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.