Encoding Featherweight Java with assignment and immutability using the Coq proof assistant
| Autor: | Julian Mackay, Hannes Mehnert, Lindsay Groves, Nicholas Cameron, Alex Potanin |
|---|---|
| Rok vydání: | 2012 |
| Předmět: |
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 |
| Zdroj: | 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 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|