Featherweight Generic Java formalization in Coq 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?
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.