Featherweight Java is a minimimum core calculus for Java formalized in this paper
CoqFJ is a mechanization of the standard theorems for type safety, i.e. progress and preservation, using coq.
To compile the code, simply run make at the root folder.
You can also generate the makefile from scratch running coq_makefile -f _CoqProject -o makefile
If you use CoqIDE, make sure to enable Project File options at Edit -> Preferences -> Project Project file options are "append to arguments".
And Default name for project file _CoqProject