Back to Search
Start Over
Encoding Featherweight Java with assignment and immutability using the Coq proof assistant
- Source :
- FTfJP@ECOOP, Mackay, J, Mehnert, H, Potanin, A, Groves, L & Cameron, N 2012, Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant . in FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs . Association for Computing Machinery, pp. 11-19 . https://doi.org/10.1145/2318202.2318206
- Publication Year :
- 2012
- Publisher :
- ACM, 2012.
-
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.
- Subjects :
- Immutability
Theoretical computer science
Java
Computer science
Programming language
Proof assistant
Software_PROGRAMMINGTECHNIQUES
Object (computer science)
Mathematical proof
computer.software_genre
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Encoding (memory)
Automated theorem provers
Software_PROGRAMMINGLANGUAGES
computer
computer.programming_language
Subjects
Details
- Database :
- OpenAIRE
- Journal :
- Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs
- Accession number :
- edsair.doi.dedup.....5e70c15d726e974467a42ed8d8688093