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

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

    Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

    Abstrakt

    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.
    OriginalsprogEngelsk
    TitelFTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs
    Antal sider8
    ForlagAssociation for Computing Machinery
    Publikationsdato2012
    Sider11-19
    ISBN (Trykt)978-1-4503-1272-1
    DOI
    StatusUdgivet - 2012

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant'. Sammen danner de et unikt fingeraftryk.

    Citationsformater