The Duality of Subtyping (Artifact)

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

Thumbnail PDF

Artifact Description

  • 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


We thank the anonymous reviewers for their helpful comments.

Cite AsGet 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)



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
  • DuoTyping
  • OOP
  • Duality
  • Subtyping
  • Supertyping


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


  1. Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 2011. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail