Featherweight Generic Java formalization in Coq
I guess somewhat more realistic task would be to find Coq's formalisation of FJ itself (probably with some extensions, but not necessarily FGJ). The one which I googled easily is:


  Encoding Featherweight Java with Assignment and
  Immutability using The Coq Proof Assistant by Mackay et al. (2012)



[the paper, PDF],
[Coq sources, ZIP].


Seems a little bit more recent than the one you mentioned. They also mention Delaware et al. (your reference) in Related work section.