Featherweight Java Axiomatically

An abstract description of the data model of Featherweight Java is provided, aimed at a clear definition of the notions of object, class, instance-of and inheritance.


Ondřej Pavlata
Jablonec nad Nisou
Czech Republic
Document date
Initial releaseFebruary 16, 2016
Last major release February 16, 2016
Last updateAugust 22, 2016
(see Document history)
  1. This document has been created without any prepublication review except those made by the author himself.

Table of contents


Featherweight Java, or FJ for short, is a formalism for the description of core features of the Java programming language. It has been proposed by A. Igarashi, B.C. Pierce and P. Wadler in October 1999 [] (with a revised and extended version [] published two years later) as a minimal core calculus for modelling Java's type system. Since then, FJ became the most popular formalism of its kind, with a number of similarly named successors like Middleweight Java [], Lightweight Java [], Welterweight Java [], Extended Featherweight Java [], Feature Featherweight Java [], Featherweight Multi Java [], Imperative Featherweight Java [], Corecursive Featherweight Java [] or FeatherTrait Java [].

Being the most popular scientific simplification of the world's most popular object-oriented programming language, Featherweight Java is of importance to the foundations of object-oriented programming. It is therefore worthwhile to consider FJ from the foundational point of view and explore alternative ways in which the formalism can be described.

The present document provides such an alternative – an axiomatic description. Featherweight Java is presented as a family of mathematical structures devoid of any syntax. There are just base sorts, entities derived from these sorts via cumulative application of set-theoretic constructs and relations between the entities (some of these relations being definitory and some derived). The description aims at providing a connection between FJ and the object models described in other author's documents, in particular, the F&D model presented in [].

The what is … questions of FJ
Let us note that the primary goal of the FJ article [] [] was modelling Java's type system, focused on a possible application to Generic Java. There is no explicitly stated claim that the article is meant to provide foundations for (core features of) object-oriented programming. Such an idea appeared rather as an afterthought, promoted by the authors themselves (cf. direct treatment of a core object-oriented language based on Java on page 247 in [] or A tiny model of (Java-like) class-based OOPLs in the Table of Contents of []). As a consequence, a reader interested in foundations of OOP might miss some definitions. In particular, one might stumble on the following two questions: The article does not provide a straightforward answer in either case. After some effort (depending on the familiarity with type-theoretic conventions) the reader might figure out the following answer to (A): In FJ, object is synonymous to well-typed value. The article does not provide such identification explicitly. Instead there is just a recursive definition of a value, v ::= new C(v1, …, vn), which reads: Consequently, the reader is supposed to figure out and accept that an object is a special case of object creation. Moreover, the new keyword used in the FJ syntax can be misleading as to the identity of objects. For example, using the sample classes Pair and A from the paper's introduction, the expression new Pair(new A(), new A()) is an object (a well-typed value) with two fields, named 'fst' and 'snd', whose values are identical. (The A class, having no fields declared or inherited, has exactly one direct instance, namely new A(). That is, new does not mean new.)

The (B) question is even harder to answer. A careful reading of the text reveals that there is in fact no definition of what a class is. The text only defines class names as abstract entities, class declarations as composite syntactic forms and class table as a mapping from class names to class declarations. Starting with section 2.1 of [] (where the formal definition of FJ begins) the first occurrence of the standalone term class (not being a subterm of either class name or class declaration) appears in the following sentence on page 405:

The reader is left to hypothesize whether class is synonymous to class name (this is suggested by e.g. writing C <: D for the subtype relation between C and D) or perhaps to class declaration, or whether a class is meant to be a pair (x,y) with x being a class name and y a class declaration (no such statement appears in the text).
The objective of this document is to provide a clean abstract description of Featherweight Java. The description should focus on general foundations of OOP and thus avoid specifics of Java or of type systems. This results in the following characteristics:
Sample structure
The diagram below shows a sample FJ2 structure – a Featherweight Java structure without methods. The definitory part is delimited by brown dashed line. It is constituted by the set C of 8 classes r, A, B, S, P, Q, X and Y, together with the inheritance relation between them (indicated by green links) and instance variable declarations (the fields) which are given by assigning each class x a possibly empty dictionary x.ѥɵ() of classes. The dictionaries are denoted (ⅰ)(ⅴ) with (ⅰ) being the empty dictionary mapped to by four classes. There is also a derived dictionary x.ѥ() of inherited instance variable declarations for each class x, with the difference indicated by dotted black arrows. (Both P and Q inherit ('fst',A) from S.)
class X extends Object { X fst; }
class Y extends Object {}
class A extends Object {}
class B extends A {}
class S extends Object { A fst; }
class P extends S { A snd; }
class Q extends S { B snd; }

(ⅰ) = = rɵ() = Aɵ() = Bɵ() = Yɵ()
(ⅱ) = {('fst', A)} = Sɵ()
(ⅲ) = {('snd', A)} = Pɵ()
(ⅳ) = {('snd', B)} = Qɵ()
(ⅴ) = {('fst', X)}

O = O2 O1
O1 = {a,b,c,d} where a = (A,), b = (B,), c = (r,), d = (Y,),
O2 O1 = {e,f,g,h,i,j,k} where e = (S,α), f = (Q,β), g = (P,β), h = (P,γ), i = (P,δ), j = (Q,γ), k = (P,ε) where α = {('fst',a)}, β = {('fst',a),('snd',b)}, γ = {('fst',b),('snd',b)}, δ = {('fst',b),('snd',a)}, ε = {('fst',a),('snd',a)}
The delimited area (class structure) uniquely determines the complementary outside part: the set O of objects. The sample structure is so crafted that there are exactly 11 objects, a to k. Each object o equals a pair (x,q) where x is a class (the class of o, pointed to by a blue link) and q is a dictionary of objects (pointed to by a black link). This dictionary is subject to typing constraints given by the x.ѥ() dictionary:
  1. q has the same keys as x.ѥ(), and
  2. if (s,(y,q')) and (s,z) are key-value pairs from q and x.ѥ(), respectively, then y z.
If we restrict the structure to classes and objects (that is, we throw away the dictionaries (ⅰ)(ⅴ) and α–ε together with all links that point to or from them) then we obtain (O, C, .class, , r) which is a standard core structure of a class-based object-oriented programming language with (a) single inheritance, (b) single root class and (c) classes not being objects. The .class map (which is simultaneously the direct instance-of relation) is formed by the blue links, the inheritance relation arises as the reflexive transitive closure of green links. Furthermore, the instance-of relation, ϵ, arises as the composition (.class) ().

Note that the X class has no instances (cf. the CycList class in []). The P class can be considered as the class of all pairs of instances of A. Since A has exactly one strict descendant (the B class), P has no strict descendants, and both A and B have exactly one instance (since they provide no field declarations) it follows that there are exactly 4 instances of P, corresponding to pairs from {A,B} × {A,B}. Similarly, the 2 instances of Q corespond to pairs from {A,B} × {B}.


We will follow the notational conventions established in [] and other author's documents. In addition, we introduce special notation for finite partial maps and and ordered finite partial maps. As a result, there will be four set-theoretic operators used for the recursive definition of expressions: the cartesian product operator × for building tuples, the unary operator for building lists, and the binary operators and for building dictionaries and ordered dictionaries, respectively.

By a dictionary we mean a finite map, that is, a finite functional relation. The word dictionary is used to suggest that the elements from the domain are considered to be names or keys. We consider a (finite) list over X to be a (finite) map from a subset I of the set of natural numbers to X such that i j I implies i I. (That is, for finite lists, I = {0, 1, …, n-1} for a natural n, called the length of the list.) By an ordered dictionary we mean a pair (k,ℓ) such that k and are finite lists of the same length and, in addition, k is injective (k[i] k[j] for i j). That is, (k,ℓ) can be equivalently specified as an (q,) where q = k−1 is a dictionary and is the linear order between keys of q given by k[i] k[j]i j.

The above definitions can be more formally summarized as follows. For sets X, Y and Σ,

X × Y is the set of all (ordered) pairs (x,y) such that x X and y Y,
Σ X is the set of all dictionaries with keys from Σ and values from X,
(i.e. Σ X is the set of all finite partial maps from Σ to X)
X is the set of all finite lists of elements from X,
(i.e. X is the set of all finite partial maps from to X such that dom(ℓ) is a down-set in (, ))
Σ X is the set of all ordered dictionaries with keys from Σ and values from X.
(I.e. Σ X is the set of all pairs (k,ℓ) from Σ × X such that dom(k) = dom(ℓ) and k−1 is a dictionary.)
As already applied above, we let dom(R) denote the domain of a (possibly functional) relation R, i.e. dom(R) equals the set of all x such that (x,y) R for some y. Similarly, the range of R is denoted rng(R) and equals dom(R−1) where R−1 is the inverse of R. The relational composition operator is interpreted left-to-right, i.e. for relations R, S, the composition R S consists of all pairs (x,z) such that (x,y) R and (y,z) S for some y. We use the operator for building general (not necessarily finite) partial maps between sets, i.e. X Y equals the set of all functional relations between X and Y. The straight arrow then indicates a total map, i.e. X Y equals the set of all functional relations between X and Y.

FJ1: A finite tree of classes

(FJ1~1) is a partial order between classes.
(FJ1~2) r is the top class w.r.t. .
(FJ1~3) Every class has at most one inheritance parent.
(FJ1~4) There are only finitely many classes.
By an FJ1 structure we mean a single-sorted structure S = (C, , r) where We might also use the term root class for r as an equivalent alternative. The structure is subject to axioms in the box on the right which just say that S is a finite tree (an inheritance tree).

Let us denote .sc the reflexive transitive reduction of and call it the superclass map. Obviously, .sc is a map from C {r} to C. If x is a class different from r then x.sc is the superclass of x or also the (inheritance) parent of x. For a natural i we denote .sc(i) the i-th composition of .sc with itself. (We let .sc(0) be the identity on C.)

FJ2: Fields (instance variable declarations)

Domains → C Σ𝕚 C
owner name bound
An FJ2 structure is a two-sorted structure (C, Σ𝕚, , r, .ѥɵ()) where The last constituent can be regarded as a relational database table with three columns according to the diagram above right. Underline in owner and name indicates a primary key. Pairs (x,s) from the domain of ɵ() are called own fields. (The ɵ subscript refers to the own adjective.) If (x,s) is an own field then x.ѥɵ(s) refers to the value of ɵ() at (x,s), which is a class called the bound of (x,s). The structure is subject to the following axioms:
(FJ2~1) For every name s,   rɵ(s) is undefined.   (The root class defines no instance variables.)
(FJ2~2) The ɵ() map is finite.   (Every class defines only finitely many instance variables.)
(FJ2~3) For every classes x, y and every name s,   if x < y then at most one of x.ѥɵ(s) and y.ѥɵ(s) is defined.
Own fields are a special case of fields which are by definition all pairs (x,s) from C × Σ𝕚 such that (a,s) is an own field for some a ≥ x. Accordingly, we extend the own-field bound map ɵ() to the field bound map () defined for all fields by In particular, () is a partial map from C × Σ𝕚 to C just like ɵ(). By currying, () and ɵ() can be regarded as total maps from the set C of classes to the set Σ𝕚 C of dictionaries of classes.

Triples (x,s,y) such that x.ѥɵ(s) = y (i.e. (x,s,y) is a row of the above table) are instance variable declarations. An instance variable declaration (x,s,y) should be roughly read as the x class declares an instance variable s whose class is y or a descendant of y. This is equivalent to say that the x class has an own-field (x,s) whose bound is y. Triples (x,s,y) such that x.ѥ(s) = y are instance variable provisions. By definition, (x,s,y) is an instance variable provision iff (a,s,y) is an instance variable declaration for some (non-strict) ancestor a of x. Axiom (FJ2~3) asserts a's uniqueness. Semantically, an instance variable provision (x,s,y) is meant to impose the following constraint:

Terminology used in this statement is defined below.
Given an FJ2 structure S = (C, Σ𝕚, , r, .ѥɵ()), the set O of objects of S is defined cumulatively via stages O0, O1, as follows:
  1. O0 = .
  2. For every natural i, the (i+1)-th stage Oi+1 equals the set of all pairs (x,d) from C × (Σ𝕚 Oi) (i.e. x is a class and d is a dictionary with keys from Σ𝕚 and values from Oi) such that
    (ⅰ) d(s) is defined   ↔   x.ѥ(s) is defined,
    (ⅱ) if d(s) = (y,_) then y x.ѥ(s).
  3. O = {Oi | i < ω}.   (The set O equals the union of all finite stages.)
Conditions (ⅰ) and (ⅱ) assert well-typedness of objects. Using the terminology introduced later, the conditions can be formulated as follows. For every object o and every instance variable name s,
(ⅰ) o has an s-named instance variable the class of o has an s-named instance variable provision
(ⅱ) if o has an s-named instance variable whose value is o' (another object) and x and y are the respective classes of o and o' then y x.ѥ(s) (i.e. y is subject to the upper bound constraint provided by the s-named instance variable provision of x).
We also define the set Θ of pre-objects (corresponding to values in []) as Θ = {Θi | i < ω} where Θi are defined like Oi except that (ⅰ) and (ⅱ) are dropped. Equivalently, Θ is the smallest set X such that X = C × (Σ𝕚 X). Given this, objects are exactly the well-typed pre-objects, i.e. O is the set of all pre-objects for which (ⅰ) and (ⅱ) are recursively satisfied.

Further observations:

  1. (FJ2~1) can be equivalently replaced by any of the following:
  2. O1 = { (x,) | x.ѥ() = }.
    (The first stage equals X × {} where X is the set of all classes without instance variable provision.)
  3. Even for (arbitrarily many) multiple classes it is possible that (r,) is the only object.
    (Consider the case when all non-root classes x have at least one instance variable declaration of the form (x,s,x).)
  4. The set O can be infinite.
    (As a minimum example, consider the case where there is exactly one non-root class x and (x,s,r) is the only instance variable declaration. Define by induction an infinite sequence o0, o1, of objects: Then for every natural i,   Oi+1 = {oi}.)
Seeing objects abstractly
By establishing notation for projections of objects to their coordinates, objects can be viewed as abstract entities. For an object o = (c,d) we refer to c by o.class and call it the class of o. This defines the class map, .class, which is a total map from O to C. The instance-of relation is denoted ϵ and defined between objects and classes as the composition (.class) (), i.e. for every object o and every class c, The .class map, as an obvious subrelation of ϵ, is called direct instance-of.

As for the second coordinate, for an object o = (c,d), the object-valued dictionary d is referred to by o.ю(). By uncurrying, this defines a partial map .ю() from O × Σ𝕚 to O called instance variable valuation. That is, .ю() is such that for every object (c,d) and every name s,

Pairs (o,s) from the domain of .ю() are called instance variables. If p = (o,s) is an instance variable then s is the name of p and o.ю(s) is the value of p. Moreover, p is said to be an instance variable of o. Well-typedness of objects can be (once again) formulated as follows. For every object x and every instance variable name s,  
(ⅰ) x.ю(s) is defined x.class.ѥ(s) is defined,
(ⅱ) x.ю(s)  ϵ  x.class.ѥ(s).

FJ3: Expressions and unnamed methods

An FJ3 structure is a 4-sorted structure (C, Σ𝕚, Σ𝕞, Eʋ, , r, .ѥɵ(), ʦ) where The structure is subject to no additional axioms.
Given an FJ3 structure S = (C, Σ𝕚, …), the set E of (evaluation) expressions of S is the smallest set that equals the (necessarily disjoint) union of the following five sets. (Terms shown in parentheses are used for the elements of the sets. The term field access is a shorthand for instance variable access.)
(a) Eʋ (local variable)
(b) E × Σ𝕚 (field access)
(c) E × Σ𝕞 × E (method invocation)
(d) C × (Σ𝕚 E) (object creature)
(e) C × E (cast)
The sequence E0, E1, … of stages of E is defined recursively by E0 = and for each natural i, the set Ei+1 being equal to the (necessarily disjoint) union of sets prescribed by (a)–(e) with E replaced by Ei.

Observe that every (pre-)object is an object creature. (This sentence also explains why we prefer the term object creature over object creation.) Every local variable is an expression (from the first stage E1) but no element of any of the remaining 3 definitory sorts C, Σ𝕚 and Σ𝕞 is an expression.

Let e, f be expressions. Then e is said to be a child expression of f, written e f, if f Eʋ and for some cartesian coordinate x of f either e equals x or e is in the range of x, the latter applied if x is a list or a dictionary. (An expression f has 2 / 3 / 2 / 2 coordinates according to which of the sets (b) / (c) / (d) / (e) it belongs.) The subexpression relation is defined as the reflexive transitive closure of and denoted . Obviously, (E, ) is a partial order. The set of all child expressions (resp. subexpressions) of an expression x is denoted by x. (resp. x.).

Observation: An expression x is a pre-object   iff   every subexpression of x is an object creature.

Let e be an expression and let q be a dictionary from Eʋ E (that is, q maps some local variables to expressions). The replacement of the q's keys in e by q's values is an expression g denoted e.repl(q) and defined recursively as follows:
(a) g = q(e) if q(e) is defined,
g = e otherwise
(case e Eʋ)
(b) g = (x.repl(q), s) (case e E × Σ𝕚, e = (x,s))
(c) g = (x.repl(q), s, ℓ .repl(q)) (case e E × Σ𝕞 × E, e = (x,s,ℓ))
(d) g = (c, d .repl(q)) (case e C × (Σ𝕚 E), e = (c,d))
(e) g = (c, x.repl(q)) (case e C × E, e = (c,x))
Typing context
By a typing context we mean a (possibly empty) dictionary from Eʋ C. That is, q is a typing context if it is a function that maps a finite set of local variables to classes.
The set Π of (unnamed) methods is defined as the set of all 4-tuples m = (k,ℓ,c,e) such that
(k,ℓ) is an ordered dictionary from Eʋ C (method arguments k and their bounds )
c is from C (return value type)
e is from E (method evaluation expression)
and the following are satisfied:
(1) ʦ is not in (the range of) k   (this does not appear in method parameters),
(2) every local variable x from e. either equals ʦ or is in (the range of) k. (Therefore, x is bound in m).
Observe that k−1 is a typing context and so is (by (1)) (k−1 ℓ) {(ʦ,a)} for any class a.

Pairs (s,m) from Σ𝕞 × Π (i.e. s is a method name and m is an unnamed method) are called named methods. A method dictionary is a dictionary from Σ𝕞 Π, i.e. it is a set of named methods with unique names.

FJ4: Method declarations

C Σ𝕞 Π
owner name method
An FJ4 structure is an FJ3 structure equipped with a mapping of classes to method dictionaries. That is, there is one additional definitory constituent, .mɵ(), called own method map, such that Similarly as with ɵ(), if (a,s) is in the domain of .mɵ() then a.mɵ(s) refers to the value of .mɵ() at (a,s). We call a triple (a,s,m) such that a.mɵ(s) = m a method declaration (i.e. (a,s,m) is a row of the table on the right). There is an induced partial order relation (.mɵ(), ) of overriding between method declarations given by
The structure is subject to the following axioms:
(FJ4~1) For every method name s,   r.mɵ(s) is undefined.   (The root class defines no methods.)
(FJ4~2) The .mɵ() map is finite.   (Every class defines only finitely many methods.)
(FJ4~3) If m = (_,ℓ,c,_) and m' = (_,ℓ',c',_) are methods that appear in overriding method declarations (a,s,m) < (a',s,m') then they have the same type signature: (ℓ,c) = (ℓ',c').
(FJ4~4) If (a,s,m) is a method declaration, m = (k,ℓ,c,e) and q denotes (k−1 ℓ) {(ʦ,a)} then
  • e.type(q) c.   (In particular, e.type(q) is defined.)
The .type() map used in (FJ4~4) is introduced below. To this end we refer to the (more general) family of structures that arise by removing (FJ4~3) and (FJ4~4) as to pre-FJ4 structures.
Method provision
Similarly as with instance variable declarations, method declarations are inherited. That is, given a pre-FJ4 structure S = (C, …), there is a derived partial function .mʜ() from C × Σ𝕚 to Π, called inherited method map (or providing method map) and defined as follows. For every class x, every method name s and every unnamed method m, The corresponding relation between classes and named methods is called method provision. In addition, the same term can be used for a triple (x,s,m) such that x.mʜ(s) = m.
The type map
Given a pre-FJ4 structure S = (C, …), the (static) type map, denoted .type(), is a partial map from E × (Eʋ C) to C defined recursively as follows. Let e be an expression and q be a typing context. Then if and only if the following conditions are recursively satisfied for each case (a)–(e).
(a) e is a local variable e Eʋ
q(e) = t
(b) e is a field access e = (x,s) e E × Σ𝕚
x.type(q).ѥ(s) = t
(c) e is a method invocation e = (x,s,ℓ) e E × Σ𝕞 × E
x.type(q).mʜ(s) = (_,ℓ',t,_)   and   dom(ℓ') = dom(ℓ)   and   ℓ[i].type(q) ℓ'[i] for each i dom(ℓ)
(d) e is an object creature e = (c,d) e C × (Σ𝕚 E)
c = t   and   dom(c.ѥ()) = dom(d)   and   d(s).type(q) c.ѥ(s) for each s dom(d)
(e) e is a cast e = (c,x) e C × E
c = t and x.type(q) is defined
(If c ≥ x.type(q) then e is called an upcast, else if c < x.type(q) then e is a downcast else e is a stupid cast, all cases w.r.t. typing context q.)
If e.type(q) is defined then we also say that e is well-typed under the context q. If q is empty then e is just said to be well-typed. We also abbreviate .type() to .type. (Therefore, .type is a partial function from the set E of expressions to the set C of classes.)


  1. Every object is well-typed. Moreover, (.class) (.type), i.e. for every object x,
  2. Objects are exactly the well-typed pre-objects.
Expression evaluation
Given a pre-FJ4 structure S = (C, …), the one-step evaluation is a relation between expressions denoted (with the inverse denoted by ) and defined recursively as follows. Let e, f be expressions. Then if one of the following conditions (b)–(e) is satisfied:
(b) e is a field access e = (x,s) e E × Σ𝕚
f = (y,s) for some y such that x y   or
f = d(s) where d is a dictionary such that x = (_,d) is an object creature and d(s) is defined
(c) e is a method invocation e = (x,s,ℓ) e E × Σ𝕞 × E
f = (y,s,ℓ) for some y such that x y   or
f = (x,s,ℓ') where ℓ' = {(i,y)} and ℓ' = {(i,z)} for some i,y,z such that y z   or
f = y.repl(z) where y and z are such that the following are satisfied:
  1. x = (c,_) is an object creature,
  2. c.mʜ(s) = (k,ℓ',_,y)   (the c class provides an s-named method (k,ℓ',_,y))
  3. dom(ℓ) = dom(ℓ'),
  4. z = k−1 {(ʦ,x)}   (z is the replacement map; in particular, ʦ is to be replaced by x).
(d) e is an object creature e = (c,d) e C × (Σ𝕚 E)
f = (x,d') where d d' = {(s,y)} and d' d = {(s,z)} for some s,y,z such that y z
(e) e is a cast e = (c,x) e C × E
f = (c,y) for some y such that x y   or
f = x and x = (b,_) is an object creature such that b c
Expressions that are minimal in (E, ) (i.e. they cannot be further reduced) are said to be in normal form.


Davide Ancona, Elena Zucca, Corecursive Featherweight Java, Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, ACM, 2012
Sven Apel, Christian Kästner, Christian Lengauer, Feature Featherweight Java: A Calculus for Feature-Oriented Programming and Stepwise Refinement, Proceedings of the 7th international conference on Generative programming and component engineering, ACM, 2008/span>
Lorenzo Bettini, Sara Capecchi, Betti Venneri, Featherweight Java with multi-methods, Proceedings of the 5th international symposium on Principles and practice of programming in Java, ACM, 2007
Lorenzo Bettini, Ferruccio Damiani, Ina Schaefer, IFJ: a Minimal Imperative Variant of FJ, Technical Report 133/2010, Dipartimento di Informatica, Università di Torino, 2010 http://www.di.unito.it/~damiani/papers/tr-133-2010.pdf
Gavin Bierman, Matthew Parkinson, Andrew Pitts, MJ: An imperative core calculus for Java and Java with effects, Technical Report 563, Cambridge University Computer Laboratory, 2003
Atsushi Igarashi, Benjamin C. Pierce, Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM SIGPLAN Notices. Vol. 34. No. 10, ACM, 1999
Atsushi Igarashi, Benjamin C. Pierce, Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), 2001 http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf
Atsushi Igarashi, A featherweight approach to FOOL, ECOOP 2011–Object-Oriented Programming, Springer Berlin Heidelberg, 2011
Luigi Liquori, Arnaud Spiwack, FeatherTrait: a modest extension of Featherweight Java, ACM Transactions on Programming Languages and Systems (TOPLAS), 2008
Jonan Östlund, Tobias Wrigstad, Welterweight Java, Objects, Models, Components, Patterns, Springer Berlin Heidelberg, 2010
Ondřej Pavlata, Object Membership: The Core Structure of Object Technology, 2012–2015, http://www.atalon.cz/om/object-membership/
Ondřej Pavlata, What Is a Metaclass?, 2016, http://www.atalon.cz/om/what-is-a-metaclass/
Benjamin C. Pierce, Types and programming languages, MIT press 2002,
Reuben N. S. Rowe , Intersection Types for Class-based Object Oriented Programming, 2008
Ulrik P. Schultz, Partial evaluation for class-based object-oriented languages, Springer Berlin Heidelberg 2001

Wikipedia: The Free Encyclopedia, http://wikipedia.org
Document history
February162016 The initial release.
August222016 Minor alterations.
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License.