DARTS.10.2.6.pdf
- Filesize: 0.63 MB
- 8 pages
Document
Pure Methods for roDOT (Artifact)
Authors
Vlastimil Dort 
,
Ondřej Lhoták ,
Pavel Parízek
-
Part of:
Issue:
Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Volume: DARTS, Volume 10 (ECOOP 2024)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-12
Artifact Description
Document Identifiers
Author Details
Cite AsGet BibTex
Vlastimil Dort, Yufeng Li, Ondřej Lhoták, and Pavel Parízek. Pure Methods for roDOT (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/DARTS.10.2.6
https://doi.org/10.4230/DARTS.10.2.6
Artifact
DARTS-10-2-6-artifact-a32d393a3275275c52e0ae40115360c6.zip
(Filesize: 0.66 MB)
Artifact Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.
Abstract
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.
Subject Classification
ACM Subject Classification
- Software and its engineering → Formal language definitions
- Software and its engineering → Object oriented languages
Keywords
- type systems
- DOT calculus
- pure methods
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Vlastimil Dort and Ondřej Lhoták. Reference mutability for DOT. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference), volume 166 of LIPIcs, pages 18:1-18:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.18.
- Vlastimil Dort, Yufeng Li, Ondřej Lhoták, and Pavel Parízek. Pure methods for roDOT (an extended version). Technical Report D3S-TR-2024-01, Dep. of Distributed and Dependable Systems, Charles University, 2024. URL: https://d3s.mff.cuni.cz/files/publications/dort_pure_report_2024.pdf.
- Ifaz Kabir. themaplelab/dot-public: A simpler syntactic soundness proof for dependent object types. URL: https://github.com/themaplelab/dot-public/tree/master/dot-simpler.