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

Emneord

Featherweight Java
Mechanized Proof
Coq Proof Assistant
Object Immutability
Type System Verification

Adgang til dokumentet

10.1145/2318202.2318206

paperIndsendt manuskript, 317 KB

ToMeSo: Tools and Methods for Scalable Software Verifications
Sestoft, P. (CoI), Birkedal, L. (PI), Mehnert, H. (CoI), Jensen, J. B. (CoI), Bengtson, J. (CoI), Thamsborg, J. J. (CoI), Hartmann Jensen, M. (CoI), Sieczkowski, F. (CoI), Mehnert, H. (CoI) & Svendsen, K. (CoI)
Danmarks Frie Forskningsfond
01/03/2009 → 30/06/2013
Projekter: Projekt › Forskning

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

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

Emneord

Adgang til dokumentet

Fingeraftryk

Projekter

ToMeSo: Tools and Methods for Scalable Software Verifications

Citationsformater