Document Open Access Logo

Pure Methods for roDOT (Artifact)

Authors Vlastimil Dort , Yufeng Li, Ondřej Lhoták , Pavel Parízek

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.10.2.6.pdf
  • Filesize: 0.63 MB
  • 8 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Vlastimil Dort
  • Charles University, Prague, Czech Republic
Yufeng Li
  • University of Cambridge, UK
Ondřej Lhoták
  • University of Waterloo, Canada
Pavel Parízek
  • Charles University, Prague, Czech Republic

Funding

This work was supported by the Czech Science Foundation project 23-06506S, and by the Czech Ministry of Education, Youth and Sports project LL2325 of the ERC.CZ programme. This research was also supported by the Natural Sciences and Engineering Research Council of Canada.

Artifact

  MD5 Sum: a32d393a3275275c52e0ae40115360c6 (Get MD5 Sum)

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.

Related Article

References

  1. 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.
  2. 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.
  3. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact