Featherweight Java: A Minimal Core Calculus for Java and GJ (2002) [pdf]

Took type system and advanced compiler last year. This paper may not look very interesting but there are a lot of proof assistant softwares that verify featherweight Java's type system to show that they work. This paper also shows that there are a lot holes in Java type system even by 2002 that makes it broken. Java's type system is probably much worse now. I think it also started the trend of featherweight-X where you try to proof a subset of a language X type system to show that if you take away features y,z and etc then type system can be proven.

One year later, wildcards (? extends/? super) where added and are now known to be unsound (more holes). After that, the Java type system has not changed.

Lambdas introduced in 2014 uses a trick, lambda types are nominal types (using interfaces) with inference sugar on top so the type system has not being extended since 2004.

See also Java and Scala’s Type Systems are Unsound, discussed at https://news.ycombinator.com/item?id=13050491

Let us erase it, box it and use it.