DARTS.10.2.6.pdf
- Filesize: 0.63 MB
- 8 pages
a32d393a3275275c52e0ae40115360c6
(Get MD5 Sum)
The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.
The artifact for the paper Pure methods for roDOT (ECOOP 2024) contains the Coq mechanization of the theorems appearing in the paper, and the necessary definitions and lemmata. Additionally, the artifact contains a mechanization of the roDOT calculus presented in an earlier paper Reference mutability for DOT (ECOOP 2020). We used the calculus from this paper as the baseline for our paper, but it has not been mechanized before. The functionality of the artifact is the ability to verify the correctness of the theorems by running Coq. Our code is based on a mechanization of a soundness proof for Field Mutable DOT.
Feedback for Dagstuhl Publishing