DistributingTypes | Xuejing Huang 2021 | Distributed under the terms of the GPL-v3 license
- The companion paper can be found at https://doi.org/10.1145/3473594.
- impl/ for the Haskell implementation
- coq/ for the Coq formalization
- spec/ for the Ott specification (that is used to generate the syntax definition in Coq)
- Fig. 3 is in Algo_bcd.hs
- Fig. 9 and 10 are in Algo_duo.hs
- Algo_sub.hs implements the algorithmic subtyping defined in Fig. 6.
- Algo_alt.hs implements the algorithmic duotyping in an alternative way (discussed in Section 5.4).
-
Install GHCi.
-
Enter impl/ directory.
-
Run ghci with the code loaded. There are some example defined in each .hs that can be used to test.
ghci Algo2.hs *Main> test1 "(Int -> (Int /\\ Int)) <: (Int -> (Int /\\ Int)) Result: True"
We use LibTactics.v from the TLC Coq library by Arthur Chargueraud.
Our Coq proofs are verified in the latest version of Coq: 8.13.2.
-
Install Coq 8.13.2. The recommended way to install Coq is via
OPAM
. Refer to here for detailed steps. Or one could download the pre-built packages for Windows and MacOS via here. Choose a suitable installer according to your platform. -
Make sure
Coq
is installed (typecoqc
in the terminal, if you see "command not found" this means you have not properly installed Coq).
-
Enter coq/ directory.
-
Type
make
in the terminal to build and compile the proofs. -
You should see something like the following (suppose
>
is the prompt):coq_makefile -arg '-w -variable-collision,-meta-collision,-require-in-module' -f _CoqProject -o CoqSrc.mk COQDEP VFILES COQC LibTactics.v COQC Definitions.v
-
Definitions.v
is generated by Ott. To reproduce it (some comments will be lost), please remove it and runmake
(with Ott installed).
-
Definitions.v contains all definitions. It is generated by spec/rules.ott.
-
TypeSize.v defines the size of type and proves some straightforward lemmas in it. It helps us to do induction on the size of type.
-
LibTactics.v is a Coq library by Arthur Chargueraud. We downloaded it from here.
-
Duotyping.v is the main file. It contains most theorems and lemmas in Sec. 4: Lemma 4.1, Theorem 4.5, Theorem 4.6, Lemma 4.7, Lemma 4.8, Lemma 4.9, Theorem 4.10, and Theorem 4.11.
-
Equivalence.v relates the two declarative systems and the two algorithmic systems, respectively. It contains Theorem 4.2, Lemma 4.3, and Theorem 4.4.
-
Subtyping.v contains some lemmas about the two subtyping systems. It is not discussed in the paper. Three of them are used in the proof of Theorem 4.4 in Equivalence.v.
-
DistAnd.v justifies one statement in the paper. It shows that the rule DS-distAnd (Fig. 4) is omittable.
-
DistSubtyping.v is a stand-alone file which contains subtyping definitions and related lemmas and theorems.