4
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

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)

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.