Document Open Access Logo

The Duality of Subtyping (Artifact)

Authors Bruno C. d. S. Oliveira, Cui Shaobo, Baber Rehman

PDF
Thumbnail PDF

Artifact Description

DARTS.6.2.8.pdf
  • Filesize: 450 kB
  • 6 pages

Document Identifiers

Author Details

Bruno C. d. S. Oliveira
  • The University of Hong Kong, China
Cui Shaobo
  • University of California San Diego, CA, USA
Baber Rehman
  • The University of Hong Kong, China

Funding

Funded by Hong Kong Research Grant Council projects number 17210617 and 17209519.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite As Get BibTex

Bruno C. d. S. Oliveira, Cui Shaobo, and Baber Rehman. The Duality of Subtyping (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 8:1-8:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/DARTS.6.2.8

Artifact

  MD5 Sum: 5dcbcfceaba4c767a6dd8611b6320c86 (Get MD5 Sum)

Abstract

This artifact contains the Coq formalization associated with the paper The Duality of Subtyping submitted in ECOOP 2020. This document explains how to run the Coq formalization. Artifact can either be compiled in the pre-built docker image with all the dependencies installed or it could be built from the scratch. Sections 1-7 explain the basic information about the artifact. Section A explains how to get the docker image for the artifact. Section B explains the prerequisites and the steps to run coq files from scratch. Section C explains coq files briefly. Section D shows the correspondence between important lemmas discussed in paper and their respective Coq formalization. The term MonoTyping used in artifact corresponds to the standard subtyping systems.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Object oriented languages
Keywords
  • DuoTyping
  • OOP
  • Duality
  • Subtyping
  • Supertyping

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Article

  • Bruno C. d. S. Oliveira, Cui Shaobo, and Baber Rehman, "The Duality of Subtyping", in 34th European Conference on Object-Oriented Programming (ECOOP 2020), LIPIcs, Vol. 166, pp. 29:1 - 29:29, 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.29

References

  1. Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 2011. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact