Java's Type System

Type systems are something that I find extremely interesting- some functional programming languages have the most beautiful type systems and their connection to logic and category theory is one of my favorite things in Computer Science. But what about imperative languages? At my university we are taught Java and object oriented programming in the imperative tradition, so I've been thinking about how to describe Java's type system. I am not an expert, and all of this has been studied before- there are extensions to the lambda calculus with order relationships and much more advanced methods of describing class based object oriented systems. These are just my idle thoughts.
First of all, there is a countably infinite set of possible types. Types can be related by a relation called sub-classing which gives us a partial order. We could describe this as saying that a class A is a sub-class of a class B iff either that fact is given by the subclass relation or there is a chain of classes c0 <= c1 <= ... <= cn such that A <= c0 and cn <= B. The ability to cast an object to another type indicates that the first type is a subclass of the second.
We also have predicates on types in the form of interfaces. For any type we can ask "does it implement some interface?". Notice that if any super class of a class implements an interface than that subclass is said to implement the interface.
For any two class, indeed any set of classes, there is a join defined as the "smallest" class that is a superclass of all classes in the set. Since there is a top element, Object, there is a join for all collections of classes. It is useful to use the ability to cast to describe the order relation rather then sub-classing, because want that x <= x, and it sounds a bit odd to say that a class is a sub-class of itself (though I don't really see anything wrong with saying that). It is certainly true however that a class A can be cast to itself, so the reflective property is obvious there. There is the problem that an object can be cast up and then cast down, but lets ignore objects and just think about types (classes).
There is no bottom class, but it is possible for a chain of classes to have an end for which no class is smaller than that bottom element of the chain- in the case that the smallest class is declared "final".
The only meets that exist are within a chain- so only the trivial meets. Many sets of types have no meet, and this captures the fact that there is only single class sub-classing- there is no multiple inheritance.
We have a universal quantifier on types in the form of generics and we can bound that type variable with the order relation ( forall A <= some class B) or by asking to to satisfy some predicate (A implements some interface B). Generic classes can be considered an indexed family of classes, with one class in the family for all Java types. Since we can have many generic parameters to a class which can be distinguished by their order we can have an indexed family(indexed by the natural numbers) of type parameters.
I'm not entirely sure what the effects of wildcards are- my understanding is that they are a little like existential types.
It seems like abstract classes have no special structure here except maybe that an abstract class with no subclasses can be see as an empty type and therefore false. The problem here is that can always make a subclass- the only way to force a class to have no subtypes is to make it final, which is not allowed for abstract class for exactly this reason.

So, that was fun! I've seen some literature about this but I've never actually looked into it yet- I'm currently more interested in languages that are more aware of their type systems like Haskell.