Title of the ECOOP 2022 paper: Union Types with Disjoint Switches
This artifact contains the mechanical formalization of the calculi associated with the paper Union Types with Disjoint Switches. All of the metatheory has been formalized in Coq theorem prover. We provide a docker image as well the code archive.
We claim the functional, reusable, and available badges.
For authors claiming a functional or reusable badge: What are claims about the artifact’s functionality to be evaluated by the committee?
All of the metatheory and theorems stated in paper can be found in the artifact.
Note: Please follow the steps under Getting Started to access the artifact and look into the directory hierarchy.
There are 4 sub-folders in the artifact in code folder:
- section3
- section4
- section51
- section52
Each folder contains Coq formalization for a variant of our calculus discussed in paper. Organization of folders is:
| Folder | System | Reference in paper |
|---|---|---|
| section3 | Union calculus | Discussed in section 3 |
| section4 | Union calculus with various advance features | Discussed in section 4 |
| section51 | An extension with parametric polymorphism | Discussed in section 5.1 |
| section52 | An extension with generalized subtyping | Discussed in section 5.2 |
Note: Note that section 5 in extended version of the paper corresponds to appendix A in ECOOP 2022 publication.
- syntax.v contains syntax and disjointness properties of the union calculus.
- typing.v contains semantics and properties related to type-safety and determinism.
Important lemmas/theorems in folder section3 and reference in section 3 in the paper:
| Lemma in Paper | Coq file | Lemma(s) in Coq File |
|---|---|---|
| Lemma 3 | syntax.v | BL_soundness and BL_completeness |
| Theorem 5 | syntax.v | Disj_soundness and Disj_completeness |
| Theorem 7 | typing.v | preservation |
| Theorem 8 | typing.v | progress |
| Theorem 10 | typing.v | determinism |
| Lemma 12 | syntax.v | disj1_disj |
- disjointness.v contains disjointness properties of the union calculus with intersection types, nominal types and distributive subtyping.
- typing.v contains semantics and properties related to type-safety and determinism.
- equivalence.v contains distributive subtyping.
Important lemmas/theorems in folder section4 and reference in section 4 in the paper:
| Lemma in Paper | Coq file | Lemma(s) in Coq File |
|---|---|---|
| Lemma 13 | equivalence.v | algo_sub_arrow_inv |
| Lemma 14 | equivalence.v | dsub2asub |
| Lemma 15 | equivalence.v | decidability |
| Theorem 18 | disjointness.v | Disj_soundness and Disj_completeness |
| Lemma 19 | disjointness.v | elem_in_findsubtypes_sub |
| Lemma 20 | disjointness.v | ord_in_findsubtypes |
| Theorem 21 | typing.v | preservation |
| Theorem 22 | typing.v | progress |
| Theorem 23 | typing.v | determinism |
Note: Note that section 5 in extended version of the paper corresponds to appendix A in ECOOP 2022 publication.
- syntax.v contains syntax and disjointness properties of the union calculus with parametric polymorphism, intersection types and nominal types.
- typing.v contains semantics and properties related to type-safety and determinism.
Important lemmas/theorems in folder section51 and reference in section 5.1 in the paper:
| Lemma in Paper | Coq file | Lemma(s) in Coq File |
|---|---|---|
| Lemma 25 | typing.v | disj_subst |
| Lemma 26 | typing.v | disj_narrowing |
- syntax.v contains syntax and disjointness properties of the union calculus with intersection types, nominal types and general subtyping rule.
- typing.v contains semantics and properties related to type-safety and determinism.
Important lemmas/theorems in folder section52 and reference in section 5.2 in the paper:
| Lemma in Paper | Coq file | Lemma(s) in Coq File |
|---|---|---|
| Lemma 27 | syntax.v | bot_sub_all |
| Lemma 28 | syntax.v | disj_bot_like |
For authors claiming a reusable badge: What are the authors' claims about the artifact's reusability to be evaluated by the committee?
More features can be added in the metatheory. For example, merge operator and disjoint intersection types. This is also discussed in Section 6 in the paper.
We agree to publish under a Creative Commons license on DARTS.
We tested all the Coq files using Coq version 8.13.1. Please use same version for the sake of consistency.
Coq TLC and Coq Metatheory libraries are also required to run the artifact.
We provide two alternatives to run the artifact:
- Docker Image
- Build From Scratch
This is the easiest way to run the artifact. We provide a docker image with all the dependencies installed in it.
This section explains how to pull the docker image of artifact from docker repo and use it. Run the following commands one by one in terminal:
$ docker pull baberrehman/switches$ docker run -it baberrehman/switches
Note: Please note that $ symbol appearing in the beginning is not a part of the command.
The artifact is located in the directory: /home/coq/code
$ cd /home/coq/code
There are 4 folders in the artifact, with make file in each.
- section3 → Discussed in section 3 in paper
- section4 → Discussed in section 4 in paper
- section51 → Discussed in section 5.1 in paper
- section52 → Discussed in section 5.2 in paper
Go to each folder and run make:
$ cd /home/coq/code/section3$ make
$ cd /home/coq/code/section4$ make
Note that compilation of equivalence.v takes a few minutes to complete.
$ cd /home/coq/code/section51$ make
$ cd /home/coq/code/section52$ make
Please feel free to go through the code in each section. vim and cat commands are available to look into the files. Recommended way to look into the files is by downloading the code archive from the given git repo.
This completes the evaluation of artifact following docker image.
This section explains how to build the artifact from scratch.
We tested all the Coq files using Coq version 8.13.1. Please use same version for the sake of consistency. We recommend installing Coq using the opam package installer.
$ opam install coq.8.13.1
Refer to this link for more information and installation steps: https://coq.inria.fr/opam-using.html
Coq TLC and Coq Metatheory libraries are required to compile the code. Next, we explain briefly how to install each.
TLC library can also be installed using the opam package installer.
Run the following commands one by one to install TLC by opam package installer:
$ opam repo add coq-released http://coq.inria.fr/opam/released$ opam install coq-tlc.20210316
Please refer to this link for detailed compilation and installation of Coq TLC: https://github.com/charguer/tlc/tree/20210316
Metatheory can be installed by following the instructions at this link: https://github.com/plclub/metalib. Metatheory library from branch coq8.10 must be installed.
Use the following commands to clone our git repo. Please note that $ symbol is not a part of command:
$ git clone https://github.com/baberrehman/disjoint-switches.git
You should be able to see all the Coq files inside folder code after cloning the repo. Alternatively you can download the zip file from repo and you should be able to see all the Coq files after unzipping it.
There are 4 sub-folders in the code folder, with make file in each.
- section3 → Discussed in section 3 in paper
- section4 → Discussed in section 4 in paper
- section51 → Discussed in section 5.1 in paper
- section52 → Discussed in section 5.2 in paper
Note: Please make sure to run $ eval $(opam env) if Coq
is installed using opam. This command can be skipped otherwise.
Open the terminal in each folder and run make:
$ eval $(opam env)(optional)$ make
Similarly, section4, section51 and section52 can be compiled
by opening the terminal in each respective folder and
running the make command.
Please feel free to go through the code in each section. This completes the evaluation of artifact following build from scratch.