I've been searching for some nice formalization of FGJ (Featherweight Generic Java) in Coq. I am going to develop an extension of FGJ in Coq, so I hope there is an appropriate Coq implementation which I can base my work on.I have found this one. I haven't yet read corresponding paper carefully, but it looks like a whole framework for building up FGJ extensions. The Coq files seem to be quite difficult to dive in (probably after reading the paper they'll become clearer).Is anybody aware of another Coq formalizations of FGJ? 
Featherweight Generic Java formalization in Coq
type theory;type systems;coq