Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant

Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, Nicholas Cameron

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    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 languageEnglish
    Title of host publicationFTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs
    Number of pages8
    PublisherAssociation for Computing Machinery
    Publication date2012
    Pages11-19
    ISBN (Print)978-1-4503-1272-1
    DOIs
    Publication statusPublished - 2012

    Fingerprint

    Dive into the research topics of 'Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant'. Together they form a unique fingerprint.

    Cite this