We develop a mechanized proof of Featherweight Java with Assignment and Immutability in the Coq proof assistant. This is a step towards more machine-checked proofs of a non-trivial type system. We used object immutability close to that of IGJ  . We describe the challenges of the mech- anisation and the encoding we used inside of Coq.
|Title of host publication||FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs|
|Number of pages||8|
|Publisher||Association for Computing Machinery|
|Publication status||Published - 2012|