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

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

doi:10.1145/2318202.2318206

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 chapter › Article in proceedings › Research › peer-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 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	https://doi.org/10.1145/2318202.2318206
Publication status	Published - 2012

Access to Document

10.1145/2318202.2318206

paperSubmitted manuscript, 317 KB

Cite this

@inproceedings{d9abdfd999354053a01e086170969839,

title = "Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant",

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.",

author = "Julian Mackay and Hannes Mehnert and Alex Potanin and Lindsay Groves and Nicholas Cameron",

year = "2012",

doi = "10.1145/2318202.2318206",

language = "English",

isbn = "978-1-4503-1272-1 ",

pages = "11--19",

booktitle = "FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs",

publisher = "Association for Computing Machinery",

address = "United States",

}

Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant. / Mackay, Julian; Mehnert, Hannes; Potanin, Alex et al.

FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs . Association for Computing Machinery, 2012. p. 11-19.

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

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

AU - Mackay, Julian

AU - Mehnert, Hannes

AU - Potanin, Alex

AU - Groves, Lindsay

AU - Cameron, Nicholas

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

U2 - 10.1145/2318202.2318206

DO - 10.1145/2318202.2318206

M3 - Article in proceedings

SN - 978-1-4503-1272-1

SP - 11

EP - 19

BT - FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs

PB - Association for Computing Machinery

ER -

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

Abstract

Access to Document

Fingerprint

Cite this