Extensible core Featherweight JavaCore Featherweight Java (cFJ) is a variant of Featherweight Java without casts. This Coq development is meant to demonstrate how to design mechanized metatheory definitions and proofs in an extensible way. There are a number of different features that can be added to uFJ to build new variants of the language. These proofs were checked with Coq version version 8.3pl2. Earlier versions of Coq might
