Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant
- Julian Mackay,
- Hannes Mehnert,
- Alex Potanin,
- Lindsay Groves,
- Nicholas Cameron
- Victoria University of Wellington,
- Mozilla Corporation
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-review
Open access
Publication Information
Output type
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 11-19 (8 pages)Publication milestones
- Published - 2012
Publication status
Published - 2012
Publisher
Association for Computing Machinery, United StatesISBN (Print)
978-1-4503-1272-1 Publication IDs
- Scopus: 84864498080
Host publication title
FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs 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.
Publication metrics
PlumX, opens in new tab
Citations
12
Captures
12
Access to documents
Submitted manuscript, 316.72 KB