Abstract
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 [9] . We describe the challenges of the mech- anisation and the encoding we used inside of Coq.
Original language | English |
---|---|
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 date | 2012 |
Pages | 11-19 |
ISBN (Print) | 978-1-4503-1272-1 |
DOIs | |
Publication status | Published - 2012 |