Encoding Featherweight Java with assignment and immutability using the Coq proof assistant
Date
Authors
Mackay, Julian
Mehnert, Hannes
Potanin, Alex
Groves, Lindsay
Cameron, Nicholas
Journal Title
Journal ISSN
Volume Title
Publisher
Association for Computing Machinery (ACM)
Access Statement
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 mechanisation and the encoding we used inside of Coq.
Description
Keywords
Citation
Collections
Source
Type
Book Title
Proceedings for FTfJP 2012: The 14th Workshop on Formal Techniques for Java-Like Programs - Co-located with ECOOP 2012 and PLDI 2012, Papers Presented at the Workshop
Entity type
Publication