Featherweight Java.
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.
Introduction
"Inside every large language is a small language
struggling to get out."
Formal modeling can offer a significant boost to the design
of complex real-world artifacts such as programming
languages. A formal model may be used to describe
some aspect of a design precisely, to state and
prove its properties, and to direct attention to issues
that might otherwise be overlooked. In formulating a
model, however, there is a tension between completeness
and compactness: the more aspects the model addresses
at the same time, the more unwieldy it becomes. Often
it is sensible to choose a model that is less complete but
more compact, offering maximum insight for minimum
investment. This strategy may be seen in a flurry of
recent papers on the formal properties of Java, which
omit advanced features such as concurrency and reflection
and concentrate on fragments of the full language
to which well-understood theory can be applied.
We propose Featherweight Java, or FJ, as a new contender
for a minimal core calculus for modeling Java's
type system. The design of FJ favors compactness over
completeness almost obsessively, having just five forms
of expression: object creation, method invocation, field
access, casting, and variables. Its syntax, typing rules,
and operational semantics fit comfortably on a single
page. Indeed, our aim has been to omit as many features
as possible - even assignment - while retaining
the core features of Java typing. There is a direct correspondence
between FJ and a purely functional core of
Java, in the sense that every FJ program is literally an
executable Java program.
FJ is only a little larger than Church's lambda calculus
[3] or Abadi and Cardelli's object calculus [1],
and is significantly smaller than previous formal models
of class-based languages like Java, including those put
forth by Drossopoulou, Eisenbach, and Khurshid [?],
Syme [20], Nipkow and Oheimb [17], and Flatt, Krish-
namurthi, and Felleisen [14]. Being smaller, FJ lets us
focus on just a few key issues. For example, we have
discovered that capturing the behavior of Java's cast
construct in a traditional "small-step" operational semantics
is trickier than we would have expected, a point
that has been overlooked or underemphasized in other
models.
One use of FJ is as a starting point for modeling
languages that extend Java. Because FJ is so compact,
we can focus attention on essential aspects of the exten-
sion. Moreover, because the proof of soundness for pure
FJ is very simple, a rigorous soundness proof for even a
significant extension may remain manageable. The second
part of the paper illustrates this utility by enriching
FJ with generic classes and methods 'a la GJ [7]. Al-
though, the model omits a few important aspects of GJ
(such as "raw types" and type argument inference for
generic method calls), it has already revealed portions
of the design that were underspecified and bugs in the
GJ compiler.
Our main goal in designing FJ was to make a proof of
type soundness ("well-typed programs don't get stuck'')
as concise as possible, while still capturing the essence
of the soundness argument for the full Java language.
Any language feature that made the soundness proof
longer without making it significantly different was a
candidate for omission. As in previous studies of type
soundness in Java, we don't treat advanced features
such as concurrency, inner classes, and reflection. Other
Java features omitted from FJ include assignment, in-
terfaces, overloading, messages to super, null pointers,
base types (int, bool, etc.), abstract method declara-
tions, shadowing of superclass fields by subclass fields,
access control (public, private, etc.), and exceptions.
The features of Java that we do model include mutually
recursive class definitions, object creation, field access,
method invocation, method override, method recursion
through this, subtyping, and casting.
One key simplification in FJ is the omission of as-
signment. We assume that an object's fields are initialized
by its constructor and never changed afterwards.
This restricts FJ to a "functional" fragment of Java,
in which many common Java idioms, such as use of
enumerations, cannot be represented. Nonetheless, this
fragment is computationally complete (it is easy to encode
the lambda calculus into it), and is large enough
to include many useful programs (many of the programs
in Felleisen and Friedman's Java text [12] use a purely
functional style). Moreover, most of the tricky typing
issues in both Java and GJ are independent of assign-
ment. An important exception is that the type inference
algorithm for generic method invocation in GJ has some
twists imposed on it by the need to maintain soundness
in the presence of assignment. This paper treats a simplified
version of GJ without type inference.
The remainder of this paper is organized as follows.
Section 2 introduces the main ideas of Featherweight
Java, presents its syntax, type rules, and reduction
rules, and sketches a type soundness proof. Section 3
extends Featherweight Java to Featherweight GJ, which
includes generic classes and methods. Section 4 presents
an erasure map from FGJ to FJ, modeling the techniques
used to compile GJ into Java. Section 5 discusses
related work, and Section 6 concludes.
In FJ, a program consists of a collection of class definitions
plus an expression to be evaluated. (This expression
corresponds to the body of the main method in
Java.) Here are some typical class definitions in FJ.
class Pair extends Object -
Object fst;
Object snd;
Pair(Object fst, Object snd) -
Pair setfst(Object newfst) -
return new Pair(newfst, this.snd);
class A extends Object -
class B extends Object -
For the sake of syntactic regularity, we always include
the supertype (even when it is Object), we always
write out the constructor (even for the trivial classes
A and B), and we always write the receiver for a field
access (as in this.snd) or a method invocation. Constructors
always take the same stylized form: there is
one parameter for each field, with the same name as the
field; the super constructor is invoked on the fields of
the supertype; and the remaining fields are initialized
to the corresponding parameters. Here the supertype is
always Object, which has no fields, so the invocations
of super have no arguments. Constructors are the only
place where super or = appears in an FJ program. Since
FJ provides no side-effecting operations, a method body
always consists of return followed by an expression, as
in the body of setfst().
In the context of the above definitions, the expres-
sion
new Pair(new A(), new B()).setfst(new B())
evaluates to the expression
new Pair(new B(), new B()).
There are five forms of expression in FJ. Here, new A(),
new B(), and new Pair(e1,e2) are object constructors,
and e3.setfst(e4) is a method invocation. In the body
of setfst, the expression this.snd is a field access, and
the occurrences of newfst and this are variables. FJ
differs from Java in that this is an ordinary variable
rather than a special keyword.
The remaining form of expression is a cast. The
expression
((Pair)new Pair(new Pair(new A(), new B()),
new A()).fst).snd
evaluates to the expression
new B().
Here, ((Pair)e7), where e7 is new Pair(.fst, is
a cast. The cast is required, because e7 is a field access
to fst, which is declared to contain an Object, whereas
the next field access, to snd, is only valid on a Pair. At
run time, it is checked whether the Object stored in the
fst field is a Pair (and in this case the check succeeds).
In Java, one may prefix a field or parameter declaration
with the keyword final to indicate that it may not
be assigned to, and all parameters accessed from an inner
class must be declared final. Since FJ contains
no assignment and no inner classes, it matters little
whether or not final appears, so we omit it for brevity.
Dropping side effects has a pleasant side effect: evaluation
can be easily formalized entirely within the syntax
of FJ, with no additional mechanisms for modeling
the heap. Moreover, in the absence of side effects,
the order in which expressions are evaluated does not
affect the final outcome, so we can define the operational
semantics of FJ straightforwardly using a nondeterministic
small-step reduction relation, following long-standing
tradition in the lambda calculus. Of course,
Java's call-by-value evaluation strategy is subsumed by
this more general relation, so the soundness properties
we prove for reduction will hold for Java's evaluation
strategy as a special case.
There are three basic computation rules: one for field
access, one for method invocation, and one for casts.
Recall that, in the lambda calculus, the beta-reduction
rule for applications assumes that the function is first
simplified to a lambda abstraction. Similarly, in FJ the
reduction rules assume the object operated upon is first
simplified to a new expression. Thus, just as the slogan
for the lambda calculus is "everything is a function,"
here the slogan is "everything is an object."
Here is the rule for field access in action:
new Pair(new A(), new B()).snd \Gamma! new B()
Because of the stylized form for object constructors, we
know that the constructor has one parameter for each
field, in the same order that the fields are declared. Here
the fields are fst and snd, and an access to the snd field
selects the second parameter.
Here is the rule for method invocation in action (=
denotes substitution):
new Pair(new A(), new B()).setfst(new B())
\Gamma!
new B()=newfst;
new Pair(new A(),new B())=this
new Pair(newfst, this.snd)
i.e., new Pair(new B(),
new Pair(new A(), new B()).snd)
The receiver of the invocation is the object
new Pair(new A(), new B()), so we look up the
setfst method in the Pair class, where we find
that it has formal parameter newfst and body
new Pair(newfst, this.snd). The invocation reduces
to the body with the formal parameter replaced by
the actual, and the special variable this replaced
by the receiver object. This is similar to the beta
rule of the lambda calculus, (x.e0)e1 \Gamma! [e1=x]e0.
The key differences are the fact that the class of
the receiver determines where to look for the body
(supporting method override), and the substitution of
the receiver for this (supporting "recursion through
self"). Readers familiar with Abadi and Cardelli's
Object Calculus will see a strong similarity to their &
reduction rule [1]. In FJ, as in the lambda calculus and
the pure Abadi-Cardelli calculus, if a formal parameter
appears more than once in the body this may lead
duplication of the actual, but since there are no side
effects this causes no problems.
Here is the rule for a cast in action:
(Pair)new Pair(new A(), new B())
\Gamma! new Pair(new A(), new B())
Once the subject of the cast is reduced to an object, it
is easy to check that the class of the constructor is a
subclass of the target of the cast. If so, as is the case
here, then the reduction removes the cast. If not, as in
the expression (A)new B(), then no rule applies and the
computation is stuck, denoting a run-time error.
There are three ways in which a computation may
get stuck: an attempt to access a field not declared for
the class, an attempt to invoke a method not declared
for the class ("message not understood"), or an attempt
to cast to something other than a superclass of the class.
We will prove that the first two of these never happen
in well-typed programs, and the third never happens
in well-typed programs that contain no downcasts (or
"stupid casts"-a technicality explained below).
As usual, we allow reductions to apply to any subexpression
of an expression. Here is a computation for the
second example expression, where the next subexpression
to be reduced is underlined at each step.
((Pair)new Pair(new Pair(new A(),
new B()), new A()).fst).snd
\Gamma! ((Pair)new Pair(new A(),new B())).snd
\Gamma! new Pair(new A(), new B()).snd
\Gamma! new B()
We will prove a type soundness result for FJ: if an expression
e reduces to expression e
0 , and if e is well typed,
then e
0 is also well typed and its type is a subtype of
the type of e.
With this informal introduction in mind, we may
now proceed to a formal definition of FJ.
2.1 Syntax
The syntax, typing rules, and computation rules for FJ
are given in Figure 1, with a few auxiliary functions in

Figure

2.
The metavariables A, B, C, D, and E range over class
names; f and g range over field names; m ranges over
method names; x ranges over parameter names; d and
e range over expressions; CL ranges over class decla-
rations; K ranges over constructor declarations; and M
ranges over method declarations. We write f as short-hand
for f1,. ,fn (and similarly for C, x, e, etc.) and
write M as shorthand for M1 . Mn (with no commas). We
write the empty sequence as ffl and denote concatenation
of sequences using a comma. The length of a sequence x
is written #(x). We abbreviate operations on pairs of sequences
in the obvious way, writing "C f" as shorthand
for "C 1 f1,. ,Cn fn ", and similarly "C f;" as short-hand
for "C 1 f1;. Cn fn;", and "this.f=f;" as short-hand
for "this.f1=f1;. ;this.fn=fn;". Sequences of
field declarations, parameter names, and method declarations
are assumed to contain no duplicate names.
A class table CT is a mapping from class names C
to class declarations CL. A program is a pair (CT ; e) of
a class table and an expression. To lighten the notation
in what follows, we always assume a fixed class table
CT .
The abstract syntax of FJ class declarations, constructor
declarations, method declarations, and expressions
is given at the top left of Figure 1. As in Java, we
assume that casts bind less tightly than other forms of
expression. We assume that the set of variables includes
the special variable this, but that this is never used
as the name of an argument to a method.
Every class has a superclass, declared with extends.
This raises a question: what is the superclass of the
Syntax:
CL ::= class C extends C -C f; K M
e ::= x
new C(e)
Subtyping:
class C extends D -.
Computation:
(new C(e)).f i \Gamma! e i
(R-Field)
(new C(e)).m(d)
\Gamma! [x 7! d; this 7! new C(e)]e0
(D)(new C(e)) \Gamma! new C(e)
(R-Cast)
Expression typing:
(T-Field)
stupid warning
Method typing:
class C extends D -.
Class typing:
class C extends D -C f; K M OK

Figure

1: FJ: Main definitions
Field lookup:
class C extends D -C f; K M
class C extends D -C f; K M
class C extends D -C f; K M
m is not defined in M
Method body lookup:
class C extends D -C f; K M
class C extends D -C f; K M
m is not defined in M
Valid method overriding:

Figure

2: FJ: Auxiliary definitions
Object class? There are various ways to deal with this
issue; the simplest one that we have found is to take
Object as a distinguished class name whose definition
does not appear in the class table. The auxiliary functions
that look up fields and method declarations in the
class table are equipped with special cases for Object
that return the empty sequence of fields and the empty
set of methods. (In full Java, the class Object does have
several methods. We ignore these in FJ.)
By looking at the class table, we can read off the sub-type
relation between classes. We write when C is
a subtype of D - i.e., subtyping is the reflexive and transitive
closure of the immediate subclass relation given
by the extends clauses in CT . Formally, it is defined in
the middle of the left column of Figure 1.
The given class table is assumed to satisfy some
sanity conditions: (1) CT class C. for every
dom(CT ); (3) for every
class name C (except Object) appearing anywhere in
CT , we have C 2 dom(CT ); and (4) there are no cycles
in the subtype relation induced by CT - that is, the
relation is antisymmetric.
For the typing and reduction rules, we need a few
auxiliary definitions, given in Figure 2. The fields of a
class C, written fields(C), is a sequence C f pairing the
class of a field with its name, for all the fields declared
in class C and all of its superclasses. The type of the
method m in class C, written mtype(m; C), is a pair, written
B!B, of a sequence of argument types B and a result
type B. Similarly, the body of the method m in class C,
written mbody(m; C), is a pair, written (x,e), of a sequence
of parameters x and an expression e. The predicate
override(C0!C; m; D) judges if a method m with
argument types C and a result type C0 may be defined
in a subclass of D. In case of overriding, if a method
with the same name is declared in the superclass then
it must have the same type.
2.2 Typing
The typing rules for expressions, method declarations,
and class declarations are in the right column of Figure
1. An environment \Gamma is a finite mapping from variables
to types, written x:C.
The typing judgment for expressions has the form
"in the environment \Gamma, expression e has
type C." The typing rules are syntax directed, with one
rule for each form of expression, save that there are three
rules for casts. The typing rules for constructors and
method invocations check that each actual parameter
has a type that is a subtype of the corresponding formal.
We abbreviate typing judgments on sequences in the
obvious way, writing
C1 , . , \Gamma ' en 2 Cn and writing
for
One technical innovation in FJ is the introduction
of "stupid" casts. There are three rules for type casts:
in an upcast the subject is a subclass of the target, in
a downcast the target is a subclass of the subject, and
in a stupid cast the target is unrelated to the subject.
The Java compiler rejects as ill typed an expression containing
a stupid cast, but we must allow stupid casts in
FJ if we are to formulate type soundness as a subject
reduction theorem for a small-step semantics. This is
because a sensible expression may be reduced to one
containing a stupid cast. For example, consider the fol-
lowing, which uses classes A and B as defined as in the
previous section:
(A)(Object)new B() \Gamma! (A)new B()
We indicate the special nature of stupid casts by including
the hypothesis stupid warning in the type rule for
stupid casts (T-SCast); an FJ typing corresponds to a
legal Java typing only if it does not contain this rule.
(Stupid casts were omitted from Classic Java [14], causing
its published proof of type soundness to be incorrect;
this error was discovered independently by ourselves and
the Classic Java authors.)
The typing judgment for method declarations has
the form M OK IN C, read "method declaration M is ok
if it occurs in class C." It uses the expression typing
judgment on the body of the method, where the free
variables are the parameters of the method with their
declared types, plus the special variable this with type
C.
The typing judgment for class declarations has the
form CL OK, read "class declaration CL is ok." It checks
that the constructor applies super to the fields of the
superclass and initializes the fields declared in this class,
and that each method declaration in the class is ok.
The type of an expression may depend on the type
of any methods it invokes, and the type of a method
depends on the type of an expression (its body), so it
behooves us to check that there is no ill-defined circularity
here. Indeed there is none: the circle is broken
because the type of each method is explicitly declared.
It is possible to load and use the class table before all
the classes in it are checked, so long as each class is
eventually checked.
2.3 Computation
The reduction relation is of the form e \Gamma! e 0 , read
"expression e reduces to expression e 0 in one step." We
write \Gamma!   for the reflexive and transitive closure of \Gamma!.
The reduction rules are given in the bottom left column
of

Figure

1. There are three reduction rules, one
for field access, one for method invocation, and one for
casting. These were already explained in the introduction
to this section. We write [d=x; e=y]e0 for the result
of replacing x1 by d1 , . , xn by dn , and y by e in expression
e0 .
The reduction rules may be applied at any point in
an expression, so we also need the obvious congruence
rules (if e \Gamma! e
.f, and the like), which
we omit here.
2.4 Properties
Formal definitions are fun, but the proof of the pudding
is in. well, the proof. If our definitions are sensible, we
should be able to prove a type soundness result, which
relates typing to computation. Indeed we can prove
such a result: if a term is well typed and it reduces to
a second term, then the second term is well typed, and
furthermore its type is a subtype of the type of the first
term.
2.4.1 Theorem [Subject Reduction]: If \Gamma ' e 2 C
and e \Gamma! e
Proof sketch: The main property required in the
proof is the following term-substitution lemma:
If
This is proved by induction on the derivation of \Gamma; x :
interesting case is when
the final rule used in the derivation is T-DCast. Suppose
the type of e0 is C0 and . By the induction
since D0 and C may or may not be in the subtype rela-
tion, the derivation of \Gamma ' (C)[d=x]e 2 C may involve a
stupid warning. On the other hand, if (C)e0 is derived
using T-UCast, then (C)[d=x]e will also be an upcast.
The theorem itself is now proved by induction on the
derivation of e \Gamma! e
, with a case analysis on the last
rule used. The case for R-Invk is easy, using the lemma
above. Other base cases are also straightforward, as are
most of the induction steps. The only interesting case is
the congruence rule for casting-that is, the case where
(C)e \Gamma! (C)e
0 is derived using e \Gamma! e
. Using an
argument similar to the term substitution lemma above,
we see that a downcast expression may be reduced to
a stupid cast and an upcast expression will be always
reduced to an upcast. \Xi
We can also show that if a program is well typed,
then the only way it can get stuck is if it reaches a
point where it cannot perform a downcast.
2.4.2 Theorem [Progress]: Suppose e is a well-typed
expression.
(1) If e includes new C0(e).f as a subexpression, then
(2) If e includes new C0(e).m(d) as a subexpression,
then mbody(m;
To state a similar property for casts, we say that an
expression e is safe in \Gamma if the type derivations of the
underlying CT and \Gamma ' e 2 C contain no downcasts
or stupid casts (uses of rules T-DCast or T-SCast).
In other words, a safe program includes only upcasts.
Then we see that a safe expression always reduces to
another safe expression, and, moreover, typecasts in a
safe expression will never fail, as shown in the following
pair of theorems.
2.4.3 Theorem: [Reduction preserves safety] If e
is safe in \Gamma and e\Gamma!e 0 , then e 0 is safe in \Gamma.
2.4.4 Theorem [Progress of safe programs]:
Suppose e is safe in \Gamma. If e has (C)new C0(e) as a
subexpression, then
3 Featherweight GJ
Just as GJ adds generic types to Java, Featherweight
GJ (or FGJ, for short) adds generic types to FJ. Here
is the class definition for pairs in FJ, rewritten with
type parameters in FGJ.
class Pair!X extends Object, Y extends Object?
extends Object -
Y snd;
!Z extends Object?
Pair!Z,Y? setfst(Z newfst) -
return new Pair!Z,Y?(newfst, this.snd);
class A extends Object -
class B extends Object -
Both classes and methods may have generic type pa-
rameters. Here X and Y are parameters of the class, and
Z is a parameter of the setfst method. Each type parameter
has a bound ; here X, Y, and Z are each bounded
by Object.
In the context of the above definitions, the expres-
sion
new Pair!A,B?(new A(), new B()).setfst!B?(new B())
evaluates to the expression
new Pair!B,B?(new B(), new B())
If we were being extraordinarily pedantic, we would
write A!? and B!? instead of A and B, but we allow the
latter as an abbreviation for the former in order that FJ
is a proper subset of FGJ.
In GJ, type parameters to generic method invocations
are inferred. Thus, in GJ the expression above
would be written
new Pair!A,B?(new A(), new B()).setfst(new B())
with no !B? in the invocation of setfst. So while FJ is
a subset of Java, FGJ is not quite a subset of GJ. We
regard FGJ as an intermediate language - the form that
would result after type parameters have been inferred.
While parameter inference is an important aspect of GJ,
we chose in FGJ to concentrate on modeling other aspects
of GJ.
The bound of a type variable may not be a type
variable, but may be a type expression involving type
variables, and may be recursive (or even, if there are
several bounds, mutually recursive). For example, if
C!X? and D!Y? are classes with one parameter each,
one may have bounds such as !X extends C!X?? or
even !X extends C!Y?, Y extends D!X??. For more
on bounds, including examples of the utility of recursive
bounds, see the GJ paper [7].
GJ and FGJ are intended to support either of two
implementation styles. They may be implemented di-
rectly, augmenting the run-time system to carry information
about type parameters, or they may be implemented
by erasure, removing all information about type
parameters at run-time. This section explores the first
style, giving a direct semantics for FGJ that maintains
type parameters, and proving a type soundness theo-
rem. Section 4 explores the second style, giving an erasure
mapping from FGJ into FJ and showing a correspondence
between reductions on FGJ expressions and
reductions on FJ expressions. The second style corresponds
to the current implementation of GJ, which compiles
GJ into the Java Virtual Machine (JVM), which of
course maintains no information about type parameters
at run-time; the first style would correspond to using
an augmented JVM that maintains information about
type parameters.
3.1
In what follows, for the sake of conciseness we abbreviate
the keyword extends to the symbol / .
The syntax, typing rules, and computation rules for
FGJ are given in Figure 3, with a few auxiliary functions
in

Figure

4. The metavariables X, Y, and Z range over
type variables; T, U, and V range over types; and N and
O range over nonvariable types (types other than type
variables). We write X as shorthand for X1,. ,Xn (and
similarly for T, N, etc.), and assume sequences of type
variables contain no duplicate names.
The abstract syntax of FGJ is given at the top left
of

Figure

3. We allow C!? and m!? to be abbreviated as
C and m, respectively.
As before, we assume a fixed class table CT , which is
a mapping from class names C to class declarations CL,
obeying the same sanity conditions as given previously.
3.2 Typing
environment \Delta is a finite mapping from type
variables to nonvariable types, written
takes each type variable to its bound.
Bounds of types
We write bound \Delta (T) for the upper bound of T in \Delta, as
defined Figure 4. Unlike calculi such as F [9], this
promotion relation does not need to be defined recur-
sively: the bound of a type variable is always a nonva-
riable type.
Subtyping
The subtyping relation is defined in the left column of

Figure

3. As before, subtyping is the reflexive and transitive
closure of the / relation. Type parameters are invariant
with regard to subtyping (for reasons explained
in the GJ paper), so does not imply
Well-formed types
If the declaration of a class C begins class C!X / N?,
then a type like C!T? is well formed only if substituting
respects the bounds N, that is if
We write well-formed in context
\Delta. The rules for well-formed types appear in Figure 3.
Note that we perform a simultaneous substitution, so
any variable in X may appear in N, permitting recursion
and mutual recursion between variables and bounds.
A type environment \Delta is well formed if \Delta ' \Delta(X) ok
for all X in dom (\Delta). We also say that an environment
\Gamma is well formed with respect to \Delta, written
if \Delta ' \Gamma(x) ok for all x in dom (\Gamma).
Field and method lookup
For the typing and reduction rules, we need a few auxiliary
definitions, given in Figure 4; these are fairly
straightforward adaptations of the lookup rules given
previously. The fields of a nonvariable type N, written
fields(N), are a sequence of corresponding types and
field names, T f. The type of the method invocation m
at nonvariable type N, written mtype(m; N), is a type of
the form !X / N?U!U. Similarly, the body of the method
invocation m at nonvariable type N with type parameters
V, written mbody(m!V?; N), is a pair, written (x,e), of a
sequence of parameters x and an expression e.
Syntax:
CL ::= class C!X / N? / N -T f; K M
e ::= x
new N(e)
Subtyping:
class C!X / N? / N -.
Well-formed types:
class C!X / N? / N -.
Computation:
(new N(e)).f i \Gamma! e i
(new N(e)).m!V?(d)
\Gamma! [d=x; new N(e)=this]e0
(O)(new N(e)) \Gamma! new N(e)
Expression typing:
stupid warning
Method typing:
class C!X / N? / N -.
Class typing:
class C!X / N? / N -T f; K M OK

Figure

3: FGJ: Main definitions
Bound of type:
bound
bound
Field lookup:
class C!X / N? / N -S f; K M
class C!X / N? / N -S f; K M
class C!X / N? / N -S f; K M
m is not defined in M
Method body lookup:
class C!X / N? / N -S f; K M
class C!X / N? / N -S f; K M
m is not defined in M
Valid method overriding:
implies

Figure

4: FGJ: Auxiliary definitions
Typing rules
Typing rules for expressions, methods, and classes appear
in Figure 3.
The typing judgment for expressions is of form
read as "in the type environment \Delta and
the environment \Gamma, e has type T." Most of the subtleties
are in the field and method lookup relations that
we have already seen; the typing rules themselves are
straightforward.
In the rule GT-DCast, the last premise ensures that
the result of the cast will be the same at run time, no
matter whether we use the high-level (type-passing) reduction
rules defined later in this section or the erasure
semantics considered in Section 4. For example, suppose
we have defined:
is, the result type of a method may be a subtype of
the result type of the corresponding method in the su-
perclass, although the bounds of type variables and the
argument types must be identical (modulo renaming of
type variables).
As before, a class table is ok if all its class definitions
are ok.
3.3 Reduction
The operational semantics of FGJ programs is only a
little more complicated than what we had in FJ. The
rules appear in Figure 3.
3.4 Properties
FGJ programs enjoy subject reduction and progress
properties exactly like programs in FJ (2.4.1 and 2.4.2).
The basic structures of the proofs are similar to those
of Theorem 2.4.1 and 2.4.2. For subject reduction, how-
ever, since we now have parametric polymorphism combined
with subtyping, we need a few more lemmas. The
main lemmas required are a term substitution lemma as
before, plus similar lemmas about the preservation of
subtyping and typing under type substitution. (Read-
ers familiar with proofs of subject reduction for typed
lambda-calculi like F [9] will notice many similarities).
We begin with the three substitution lemmas, which are
proved by straightforward induction on a derivation of
3.4.1 Lemma: [Type substitution preserves sub-
with and none of X appearing in \Delta 1 , then
3.4.2 Lemma: [Type substitution preserves typ-
and none of X appears in \Delta 1 , then
such that
3.4.3 Lemma: [Term substitution preserves typ-
such that
3.4.4 Theorem [Subject reduction]: If \Delta; \Gamma ' e 2
that
Proof By induction on the derivation of
e \Gamma! e
0 with a case analysis on the reduction rule used.
We show in detail just the base case where e is a method
invocation. From the premises of the rule GR-Invk, we
have
e
By the rule GT-Invk and GT-New, we also have
By examining the derivation of mtype(m; bound \Delta (N)),
we can find a supertype C!T? of N where
and none of the Y appear in T. Now, by Lemma 3.4.2,
From this, a straightforward weakening lemma (not
shown here), plus Lemma 3.4.3 and Lemma 3.4.1, gives
Letting T
finishes the case, since \Delta ' S
by S-Trans. \Xi
Theorem [Progress]: Suppose e is a well-typed
expression.
(1) If e includes new N0(e).f as a subexpression, then
(2) If e includes new N0(e).m!V?(d) as a subexpres-
sion, then mbody(m!V?;
#(d).
FGJ is backward compatible with FJ. Intuitively,
this means that an implementation of FGJ can be used
to typecheck and execute FJ programs without changing
their meaning. We can show that a well-typed FJ program
is always a well-typed FGJ program and that FJ
and FGJ reduction correspond. (Note that it isn't quite
the case that the well-typedness of an FJ program under
the FGJ rules implies its well-typedness in FJ, because
FGJ allows covariant overriding and FJ does not.) In
the statement of the theorem, we use \Gamma! FJ and \Gamma! FGJ
to show which set of reduction rules is used.
3.4.6 Theorem [Backward compatibility]: If an
FJ program (e; CT ) is well typed under the typing
rules of FJ, then it is also well-typed under the rules of
FGJ. Moreover, for all FJ programs e and e
(whether
well typed or not), e \Gamma! FJ e
Proof: The first half is shown by straightforward induction
on the derivation of \Gamma ' e 2 C (using FJ typing
rules), followed by an analysis of the rules GT-Method
and GT-Class. In the second half, both directions are
shown by induction on a derivation of the reduction re-
lation, with a case analysis on the last rule used. \Xi
Compiling FGJ to FJ
We now explore the second implementation style for GJ
and FGJ. The current GJ compiler works by translation
into the standard JVM, which maintains no information
about type parameters at run-time. We model this
compilation in our framework by an erasure translation
from FGJ into FJ. We show that this translation maps
well-typed FGJ programs into well-typed FJ programs,
and that the behavior of a program in FGJ matches (in
a suitable sense) the behavior of its erasure under the
FJ reduction rules.
A program is erased by replacing types with their
erasures, inserting downcasts where required. A type is
erased by removing type parameters, and replacing type
variables with the erasure of their bounds. For example,
the class Pair!X,Y? in the previous section erases to the
class Pair extends Object -
Object fst;
Object snd;
Pair(Object fst, Object snd) -
Pair setfst(Object newfst) -
return new Pair(newfst, this.snd);
Similarly, the field selection
new Pair!A,B?(new A(), new B()).snd
erases to
(B)new Pair(new A(), new B()).snd
where the added downcast (B) recovers type information
of the original program. We call such downcasts
inserted by erasure synthetic.
4.1 Erasure of Types
To erase a type, we remove any type parameters and
replace type variables with the erasure of their bounds.
Write jTj \Delta for the erasure of type T with respect to type
environment \Delta
4.2 Field and Method Lookup
In FGJ (and GJ), a subclass may extend an instantiated
superclass. This means that, unlike in FJ (and Java),
the types of the fields and the methods in the subclass
may not be identical to the types in the superclass. In
order to specify a type-preserving erasure from FGJ to
FJ, it is necessary to define additional auxiliary functions
that look up the type of a field or method in the
highest superclass in which it is defined.
For example, we previously defined the generic class
Pair!X,Y?. We may declare a specialized subclass
PairOfA as a subclass of the instantiation Pair!A,A?,
which instantiates both X and Y to a given class A.
class PairOfA extends Pair!A,A? -
super(fst, snd);
PairOfA
return new PairOfA(newfst, this.fst);
Note that, in the setfst method, the argument type
A matches the argument type of setfst in Pair!A,A?,
while the result type PairOfA is a subtype of the result
type in Pair!A,A?; this is permitted by FGJ's covariant
subtyping, as discussed in the previous section. Erasing
the class PairOfA yields the following:
class PairOfA extends Pair -
PairOfA(Object fst, Object snd) -
super(fst, snd);
Pair setfst(Object newfst) -
return new PairOfA(newfst, this.fst);
Here arguments to the constructor and the method are
given type Object, even though the erasure of A is itself;
and the result of the method is given type Pair, even
though the erasure of PairOfA is itself. In both cases,
the types are chosen to correspond to types in Pair, the
highest superclass in which the fields and method are
defined.
We define variants of the auxiliary functions that
find the types of fields and methods in the highest superclass
in which they are defined. The maximum field
types of a class C, written fieldsmax (C), is the sequence
of pairs of a type and a field name defined as follows:
class C!X / N? / D!U? -T f; .
The maximum method type of m in C, written
(m, C), is defined as follows:
class C!X / N? / D!U? -.
class C!X / N? / D!U? -.
undefined
We also need a way to look up the maximum type
of a given field. If fieldsmax then we set
4.3 Erasure of Expressions
The erasure of an expression depends on the typing of
that expression, since the types are used to determine
which downcasts to insert. The erasure rules are optimized
to omit casts when it is trivially safe to do so;
this happens when the maximum type is equal to the
erased type.
Write jej \Delta;\Gamma for the erasure of a well-typed expression
e with respect to environment \Gamma and type environment
\Delta:
jnew N(e)j
(Strictly speaking, one should think of the erasure
operation as acting on typing derivations rather than
expressions. Since well-typed expressions are in 1-1 correspondence
with their typing derivations, the abuse of
notation creates no confusion.)
4.4 Erasure of Methods and Classes
The erasure of a method m with respect to type environment
\Delta in class C, written jMj \Delta;C , is defined as follows:
e
(In GJ, the actual erasure is somewhat more complex,
involving the introduction of bridge methods, so that
one ends up with two overloaded methods: one with
the maximum type, and one with the instantiated type.
We don't model that extra complexity here, because it
depends on overloading of method names, which is not
modeled in FJ.)
The erasure of constructors and classes is:
jclass C!X / N? / N -T f; K Mj
class C / jNj
4.5 Properties of Erasure
Having defined erasure, we may investigate some of its
properties. First, a well-typed FGJ program erases to a
well-typed FJ program, as expected:
4.5.1 Theorem [Erasure preserves typing]: If an
FGJ class table CT is ok and \Delta; \Gamma ' e 2 T, then
using FJ rules.
Proof By induction on the derivation of
using the following lemmas: (1) if
if \Delta ' N ok and methodtype FGJ (m;
then mtypemax (m; jNj
some well-formed type environment \Delta, then
More interestingly, we would intuitively expect that
erasure from FGJ to FJ should also preserve the reduction
behavior of FGJ programs:
e
reduce
erase
eerase
reduce
Unfortunately, this is not quite true. For example, consider
the FGJ expression
where a and b are expressions of type A and B, respec-
tively, and its erasure:
(A)new Pair(jaj \Delta;\Gamma ,jbj \Delta;\Gamma ).fst
In FGJ, e reduces to jaj \Delta;\Gamma , while the erasure jej \Delta;\Gamma reduces
to (A)jaj \Delta;\Gamma in FJ; it does not reduce to jaj \Delta;\Gamma
when a is not a new expression. (Note that it is not
an artifact of our nondeterministic reduction strategy:
it happens even if we adopt a call-by-value reduction
strategy, since, after method invocation, we may obtain
an expression like (A)e where e is not a new expres-
sion.) Thus, the above diagram does not commute even
if one-step reduction (\Gamma!) at the bottom is replaced
with many-step reduction (\Gamma!   ). In general, synthetic
casts can persist for a while in the FJ expression, although
we expect those casts will eventually turn out
to be upcasts when a reduces to a new expression.
In the example above, an FJ expression d reduced
from jej \Delta;\Gamma had more synthetic casts than je
ever, this is not always the case: d may have less casts
than je when the reduction step involves method
invocation. Consider the following class and its erasure:
class C!X extends Object? extends Object -
return new C!X?(this.f);
class C extends Object -
Object f;
C(Object f) -
return new C(this.f);
Now consider the FGJ expression
new C!A?(new A()).m()
and its erasure
new C(new A()).m():
In FGJ,
e \Gamma! FGJ new C!A?(new C!A?(new A()).f):
In FJ, on the other hand, jej \Delta;\Gamma reduces to
new C(new C(new A()).f), which has fewer synthetic
casts than new C((A)new C(new A()).f), which is the
erasure of the reduced expression in FGJ. The subtlety
we observe here is that, when the erased term is re-
duced, synthetic casts may become "coarser" than the
casts inserted when the reduced term is erased, or may
be removed entirely as in this example. (Removal of
downcasts can be considered as a combination of two
operations: replacement of (A) with the coarser cast
(Object) and removal of the upcast (Object), which
does not affect the result of computation.)
To formalize both of these observations, we define an
auxiliary relation that relates FJ expressions differing
only by the addition and replacement of some synthetic
casts. Let us call a well-typed expression d an expansion
of a well-typed expression e, written e =) d, if d is
obtained from e by some combination of (1) addition of
zero or more synthetic upcasts, (2) replacement of some
synthetic casts (D) with (C), where C is a supertype of
D, or (3) removal of some synthetic casts.
4.5.2 Theorem: [Erasure preserves reduction
modulo expansion] If \Delta; \Gamma ' e 2 T and e \Gamma! FGJ

e
, then there exists some FJ expression d
0 such that
0 and jej \Delta;\Gamma \Gamma! FJ d
0 . In other words, the
following diagram commutes.
e
reduce
erase
erase
reduce

d
As easy corollaries of this theorem, it can be shown that,
if an FGJ expression e reduces to a "fully-evaluated
expression," then the erasure of e reduces to exactly
its erasure, and that if FGJ reduction gets stuck at a
stupid cast, then FJ reduction also gets stuck because
of the same typecast. We use the metavariable v for
fully evaluated expressions, defined as follows:
4.5.3 Corollary: [Erasure preserves execution
results] If \Delta; \Gamma ' e 2 T and e \Gamma! FGJ
v, then
jvj \Delta;\Gamma .
4.5.4 Corollary: [Erasure preserves typecast er-
e
ehas a stuck subexpression (C!S?)new D!T?(e), then
d
0 such that d
0 has a stuck subexpression
(C)new D(d), where d are expansions of the erasures of
e, in the same position (modulo synthetic casts) as the
erasure of e
5 Related Work
Core calculi for Java. There are several known
proofs in the literature of type soundness for subsets
of Java. In the earliest, Drossopoulou and Eisenbach
[11] (using a technique later mechanically checked
by Syme [20]) prove soundness for a fairly large subset
of sequential Java. Like us, they use a small-step operational
semantics, but they avoid the subtleties of "stupid
casts" by omitting casting entirely. Nipkow and Oheimb
[17] give a mechanically checked proof of soundness
for a somewhat larger core language. Their language
does include casts, but it is formulated using a "big-
step" operational semantics, which sidesteps the stupid
cast problem. Flatt, Krishnamurthi, and Felleisen [14]
use a small-step semantics and formalize a language
with both assignment and casting. Their system is
somewhat larger than ours (the syntax, typing, and operational
semantics rules take perhaps three times the
space), and the soundness proof, though correspondingly
longer, is of similar complexity. Their published
proof of subject reduction is slightly flawed - the case
that motivated our introduction of stupid casts is not
handled properly - but the problem can be repaired by
applying the same refinement we have used here.
Of these three studies, that of Flatt, Krishnamurthi,
and Felleisen is closest to ours in an important sense:
the goal there, as here, is to choose a core calculus that
is as small as possible, capturing just the features of
Java that are relevant to some particular task. In their
case, the task is analyzing an extension of Java with
Common Lisp style mixins - in ours, extensions of the
core type system. The goal of the other two systems, on
the other hand, is to include as large a subset of Java
as possible, since their primary interest is proving the
soundness of Java itself.
Other class-based object calculi. The literature
on foundations of object-oriented languages contains
many papers formalizing class-based object-oriented
languages, either taking classes as primitive (e.g., [21, 8,
6, 5]) or translating classes into lower-level mechanisms
(e.g., [13, 4, 1, 19]. Some of these systems (e.g. [19, 8])
include generic classes and methods, but only in fairly
simple forms.
Generic extensions of Java. A number of extensions
of Java with generic classes and methods have
been proposed by various groups, including the language
of Agesen, Freund, and Mitchell [2]; PolyJ, by
Myers, Bank, and Liskov [16]; Pizza, by Odersky and
Wadler [18]; GJ, by Bracha, Oderksy, Stoutamire, and
Wadler [7]; and NextGen, by Cartwright and Steele [10].
While all these languages are believed to be typesafe,
our study of FGJ is the first to give rigorous proof of
soundness for a generic extension of Java. We have used
GJ as the basis for our generic extension, but similar
techniques should apply to the forms of genericity found
in the rest of these languages.
6 Discussion
We have presented Featherweight Java, a core language
for Java modeled closely on the lambda-calculus and
embodying many of the key features of Java's type sys-
tem. FJ's definition and proof of soundness are both
concise and straightforward, making it a suitable arena
for the study of ambitious extensions to the type sys-
tem, such as the generic types of GJ. We have developed
this extension in detail, stated some of its fundamental
properties, and sketched their proofs.
FJ itself is not quite complete enough to model some
of the interesting subtleties found in GJ. In particular,
the full GJ language allows some parameters to be instantiated
by a special "bottom type" *, using a slightly
delicate rule to avoid unsoundness in the presence of as-
signment. Capturing the relevant issues in FGJ requires
extending it with assignment and null values (both of
these extensions seem straightforward, but cost us some
of the pleasing compactness of FJ as it stands). The
other somewhat subtle aspect of GJ that is not accurately
modeled in FGJ is the use of bridge methods in
the compilation from GJ to JVM bytecodes. To treat
this compilation exactly as GJ does, we would need to
extend FJ with overloading.
Our formalization of GJ also does not include raw
types, a unique aspect of the GJ design that supports
compatibility between old, unparameterized code and
new, parameterized code. We are currently experimenting
with an extension of FGJ with raw types.
Formalizing generics has proven to be a useful application
domain for FJ, but there are other areas where its
extreme simplicity may yield significant leverage. For
example, work is under way on formalizing Java 1.1's
inner classes using FJ [15].

Acknowledgments

This work was supported by the University of Pennsylvania
and the National Science Foundation under grant
CCR-9701826, Principled Foundations for Programming
with Objects. Igarashi is a research fellow of the Japan
Society for the Promotion of Science.



--R

A Theory of Ob- jects
Adding type parameterization to the Java language.
The Lambda Calculus.
An imperative first-order calculus with object extension
A core calculus of classes and mix- ins
A core calculus of classes and objects.
Making the future safe for the past: Adding genericity to the Java programming language.
"Safe type checking in a statically typed object-oriented programming language"
An extension of system F with subtyping.
Steele Jr.
Is the Java Type System Sound?
A little Java
On the relationship between classes
Classes and mixins.
On inner classes
Parameterized types for Java.
Java light is type-safe - definitely
Pizza into Java: Translating theory into practice.
Simple type-theoretic foundations for object-oriented pro- gramming
Proving Java type soundness.
Type inference for objects with instance variables and inheritance.
--TR
An extension of system <italic>F</italic> with subtyping
A syntactic approach to type soundness
Parameterized types for Java
Pizza into Java
Adding type parameterization to the Java language
Java<i><sub>light</sub></i> is type-safeMYAMPERSANDmdash;definitely
Classes and mixins
A little Java, a few patterns
Making the future safe for the past
Compatible genericity with run-time types for the Java programming language
On the relationship between classes, objects, and data abstraction
Is the Java type system sound?
Modular type-based reverse engineering of parameterized types in Java code
Parametric polymorphism in Java
Types and programming languages
A Theory of Objects
Partial Evaluation for Class-Based Object-Oriented Languages
An Imperative, First-Order Calculus with Object Extension
A Core Calculus of Classes and Mixins
On Inner Classes
True Modules for Java-like Languages

--CTR
Maurizio Cimadamore , Mirko Viroli, Reifying wildcards in Java using the EGO approach, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
Peter Hui , James Riely, Typing for a minimal aspect language: preliminary report, Proceedings of the 6th workshop on Foundations of aspect-oriented languages, p.15-22, March 13-13, 2007, Vancouver, British Columbia, Canada
Giovanni Rimassa , Mirko Viroli, Understanding access restriction of variant parametric types and Java wildcards, Proceedings of the 2005 ACM symposium on Applied computing, March 13-17, 2005, Santa Fe, New Mexico
Atsushi Igarashi , Hideshi Nagira, Union types for object-oriented programming, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
Marco Bellia , M. Eugenia Occhiuto, Higher order Programming in Java: Introspection, Subsumption and Extraction, Fundamenta Informaticae, v.67 n.1-3, p.29-44, January 2005
Tomoyuki Aotani , Hidehiko Masuhara, Towards a type system for detecting never-matching pointcut compositions, Proceedings of the 6th workshop on Foundations of aspect-oriented languages, p.23-26, March 13-13, 2007, Vancouver, British Columbia, Canada
Jeffrey Fischer , Rupak Majumdar , Todd Millstein, Tasks: language support for event-driven programming, Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 15-16, 2007, Nice, France
Jaakko Jrvi , Jeremiah Willcock , Andrew Lumsdaine, Associated types and constraint propagation for mainstream object-oriented generics, ACM SIGPLAN Notices, v.40 n.10, October 2005
Gustavo Bobeff , Jacques Noy, Component specialization, Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.39-50, August 24-25, 2004, Verona, Italy
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
Neal Glew , Jens Palsberg, Type-safe method inlining, Science of Computer Programming, v.52 n.1-3, p.281-306, August 2004
Tian Zhao , Jens Palsber , Jan Vite, Lightweight confinement for featherweight java, ACM SIGPLAN Notices, v.38 n.11, November
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
Alex Potanin , James Noble , Dave Clarke , Robert Biddle, Featherweight generic confinement, Journal of Functional Programming, v.16 n.6, p.793-811, November 2006
Nathaniel Nystrom , Stephen Chong , Andrew C. Myers, Scalable extensibility via nested inheritance, ACM SIGPLAN Notices, v.39 n.10, October 2004
G. M. Bierman, Formal semantics and analysis of object queries, Proceedings of the ACM SIGMOD international conference on Management of data, June 09-12, 2003, San Diego, California
Gurevich , Benjamin Rossman , Wolfram Schulte, Semantic essence of AsmL, Theoretical Computer Science, v.343 n.3, p.370-412, 17 October 2005
Ernst , Klaus Ostermann , William R. Cook, A virtual class calculus, ACM SIGPLAN Notices, v.41 n.1, p.270-282, January 2006
Todd Millstein , Colin Bleckner , Craig Chambers, Modular typechecking for hierarchically extensible datatypes and functions, ACM SIGPLAN Notices, v.37 n.9, p.110-122, September 2002
Suresh Jagannathan , Jan Vitek , Adam Welc , Antony Hosking, A transactional object calculus, Science of Computer Programming, v.57 n.2, p.164-186, August 2005
Lorenzo Bettini , Sara Capecchi , Elena Giachino, Featherweight wrap Java, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
Adriaan Moors , Frank Piessens , Wouter Joosen, An object-oriented approach to datatype-generic programming, Proceedings of the 2006 ACM SIGPLAN workshop on Generic programming, September 16-16, 2006, Portland, Oregon, USA
Christian Skalka, Trace effects and object orientation, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.139-150, July 11-13, 2005, Lisbon, Portugal
Alessandro Warth , Milan Stanojevi , Todd Millstein, Statically scoped object adaptation with expanders, ACM SIGPLAN Notices, v.41 n.10, October 2006
Dan Grossman , Jeremy Manson , William Pugh, What do high-level memory models mean for transactions?, Proceedings of the 2006 workshop on Memory system performance and correctness, October 22-22, 2006, San Jose, California
Matthew S. Tschantz , Michael D. Ernst, Javari: adding reference immutability to Java, ACM SIGPLAN Notices, v.40 n.10, October 2005
Juan Chen , David Tarditi, A simple typed intermediate language for object-oriented languages, ACM SIGPLAN Notices, v.40 n.1, p.38-49, January 2005
Polyvios Pratikakis , Jaime Spacco , Michael Hicks, Transparent proxies for java futures, ACM SIGPLAN Notices, v.39 n.10, October 2004
Marko van Dooren , Eric Steegmans, Combining the robustness of checked exceptions with the flexibility of unchecked exceptions using anchored exception declarations, ACM SIGPLAN Notices, v.40 n.10, October 2005
Franz Achermann , Oscar Nierstrasz, A calculus for reasoning about software composition, Theoretical Computer Science, v.331 n.2-3, p.367-396, 25 February 2005
Alexander Ahern , Nobuko Yoshida, Formalising Java RMI with explicit code mobility, ACM SIGPLAN Notices, v.40 n.10, October 2005
Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006
Philip W. L. Fong, Reasoning about safety properties in a JVM-like environment, Science of Computer Programming, v.67 n.2-3, p.278-300, July, 2007
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
dependent types for higher-order mobile processes, ACM SIGPLAN Notices, v.39 n.1, p.147-160, January 2004
Atsushi Igarashi , Mirko Viroli, Variant parametric types: A flexible subtyping scheme for generics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.5, p.795-847, September 2006
Alex Potanin , James Noble , Dave Clarke , Robert Biddle, Generic ownership for generic Java, ACM SIGPLAN Notices, v.41 n.10, October 2006
Daniel J. Dougherty , Pierre Lescanne , Luigi Liquori, Addressed term rewriting systems: application to a typed object calculus, Mathematical Structures in Computer Science, v.16 n.4, p.667-709, August 2006
Tian Zhao , Jens Palsberg , Jan Vitek, Type-based confinement, Journal of Functional Programming, v.16 n.1, p.83-128, January 2006
Todd Millstein , Colin Bleckner , Craig Chambers, Modular typechecking for hierarchically extensible datatypes and functions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.5, p.836-889, September 2004
Chris Andreae , James Noble , Shane Markstrum , Todd Millstein, A framework for implementing pluggable type systems, ACM SIGPLAN Notices, v.41 n.10, October 2006
Radha Jagadeesan , Alan Jeffrey , James Riely, Typed parametric polymorphism for aspects, Science of Computer Programming, v.63 n.3, p.267-296, 15 December 2006
Martin Abadi , Cormac Flanagan , Stephen N. Freund, Types for safe locking: Static race detection for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.207-255, March 2006
Einar Broch Johnsen , Olaf Owe , Ingrid Chieh Yu, Creol: a type-safe object-oriented model for distributed concurrent systems, Theoretical Computer Science, v.365 n.1, p.23-66, 10 November 2006
Anindya Banerjee , David A. Naumann, Ownership confinement ensures representation independence for object-oriented programs, Journal of the ACM (JACM), v.52 n.6, p.894-960, November 2005
language design;compilation;generic classes;language semantics