Distributing Intersection and Union Types with Splits and Duality (Artifact)

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)

Haskell Implementation

• 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).

Building Instructions

1. Install GHCi.

2. Enter impl/ directory.

3. 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"

Coq Formalization

Third Party Materials

We use LibTactics.v from the TLC Coq library by Arthur Chargueraud.

Building Instructions

Our Coq proofs are verified in the latest version of Coq: 8.13.2.

Prerequisites

1. 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.

2. Make sure Coq is installed (type coqc in the terminal, if you see "command not found" this means you have not properly installed Coq).

Build and Compile the Proofs

1. Enter coq/ directory.

2. Type make in the terminal to build and compile the proofs.

3. 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

4. Definitions.v is generated by Ott. To reproduce it (some comments will be lost), please remove it and run make (with Ott installed).

Proof Structure

• 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.