<p>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:</p>

<blockquote>
  <p>Encoding Featherweight Java with Assignment and
  Immutability using The Coq Proof Assistant <em>by Mackay et al.</em> (2012)</p>
</blockquote>

<ul>
<li><a href="https://www.cl.cam.ac.uk/~hm519/ftfjp12.pdf" rel="nofollow">[the paper, PDF]</a>,</li>
<li><a href="https://www.cl.cam.ac.uk/~hm519/FJAI.zip" rel="nofollow">[Coq sources, ZIP]</a>.</li>
</ul>

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

CC BY-SA 3.0
2016-01-12T20:26:14.540Z
2016-01-12T21:22:37.323Z
2016-01-12T21:22:37.323Z
Artem Pelenitsyn
<p>I've been searching for some nice <strong>formalization of FGJ (Featherweight Generic Java) in Coq</strong>. 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.</p>

<p>I have found <a href="http://people.csail.mit.edu/bendy/PLoTs/">this one</a>. 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).</p>

<p>Is anybody aware of another Coq formalizations of FGJ? </p>

<type-theory><type-systems><coq>
Featherweight Generic Java formalization in Coq
juliet
# Featherweight Generic Java formalization in Coq

(Asked by: username_0 on 2016-01-12)

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](http://people.csail.mit.edu/bendy/PLoTs/). 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?

**Tags:** type-theory, type-systems, coq


---

## 1 answers

### Answer by username_1 on 2016-01-12. Score: 3

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]](https://www.cl.cam.ac.uk/~hm519/ftfjp12.pdf),
* [[Coq sources, ZIP]](https://www.cl.cam.ac.uk/~hm519/FJAI.zip).

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


---

