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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs
Antal sider	8
Forlag	Association for Computing Machinery
Publikationsdato	2012
Sider	11-19
ISBN (Trykt)	978-1-4503-1272-1
DOI	https://doi.org/10.1145/2318202.2318206
Status	Udgivet - 2012

Adgang til dokumentet

10.1145/2318202.2318206

paperIndsendt manuskript, 317 KB

Citationsformater

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

keywords = "Featherweight Java, , Mechanized Proof, , Coq Proof Assistant, , Object Immutability, , Type System Verification",

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. s. 11-19.

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

KW - Featherweight Java

KW - Mechanized Proof

KW - Coq Proof Assistant

KW - Object Immutability

KW - Type System Verification

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

Adgang til dokumentet

Fingeraftryk

Citationsformater