Skip to content

Latest commit

 

History

History
130 lines (92 loc) · 7.22 KB

README_dev.md

File metadata and controls

130 lines (92 loc) · 7.22 KB
Raw

Full Iso-recursive Types

Building Instructions

Our proofs are verified in Coq version Coq 8.13.2. We rely on the Coq library: metalib for the locally nameless representation in our proofs.

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, then install Metalib:

    1. Open terminal
    2. git clone -b coq8.10 https://github.com/plclub/metalib
    3. cd metalib/Metalib
    4. make install

For checking proofs of the paper, you can already stop here and use the provided syntax_ott.v and rules_inf.v files. We have already built these files, which are generated by the LNgen and Ott tools. If you want to modify the rules, you can follow the rest of the instructions below to install LNgen and Ott:

  1. Make sure Haskell with stack is installed, then install LNgen:

    1. Open terminal
    2. git clone https://github.com/plclub/lngen
    3. cd lngen
    4. stack install

  2. Install Ott 0.32 if you want to rewrite the rules. Make sure opam is installed:

    1. Open terminal
    2. git clone https://github.com/sweirich/ott -b ln-close
    3. cd ott
    4. opam pin add ott .
    5. opam pin add coq-ott .

    Check the Ott website for detailed instructions. Remember to switch to the correct forked version of Ott 0.32 during the installation process.

Build and Compile the Proofs

  1. Enter the coq directory you would like to build.

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

Other make commands (with LNgen and Ott installed):

make rules # Generate the syntax_ott.v and rules_inf.v files
make pdf   # Generate the latex pdf from the Ott specification
make realclean # Clean all the generated files including documents
make clean # Clean all the files generated by Coq checking

Proof Structure

There are two directories in this artifact. The cast_main directory contains the proofs for the main system presented in Section 3 and Section 4 of the paper. The cast_sub directory contains the proofs for the main system extended with subtyping presented in Section 5 of the paper.

The cast_main and cast_sub share the same structure, in which all the proof files have a sequential dependency, as can be found in _CoqProject file of each directory. The proof starts from syntax_ott.v, which is generated from the Ott specification in spec directory, and ends with theorems.v. The theorems.v file contains most of the main theorems of the paper. There is also a doc directory that contains a latex pdf generated from the Ott specification that presents all the rules of each system.

In addition, within cast_sub there is a subdirectory subtyping which contains the Coq proofs from the artifact of the paper "Revisiting Iso-recursive Subtyping" (Zhou et al. 2022). We transported their results (e.g. unfolding lemma) to our setting through subtyping.v in the cast_sub directory.

Key Definitions in the Paper

Definition File Notation in Paper Name in Coq
Fig. 2. Brandt and Henglein's equi-recursive type equality syntax_ott.v $H \vdash A \doteq B$ eqe2
Fig. 4. Typing syntax_ott.v $\Gamma \vdash e: A $ Typing
Fig. 4. Type Casting syntax_ott.v $\Delta; \mathbb{E} \vdash A \hookrightarrow B : c $ TypCast
Fig. 5. Equi-recursive typing with rule Typ-eq syntax_ott.v $\Gamma \vdash_e e : A $ EquiTyping
Fig. 5. Full iso-recursive elaboration syntax_ott.v $\Gamma \vdash_e e : A \rhd e' $ EquiTypingC
Fig. 6. Reduction rules syntax_ott.v $e \hookrightarrow e' $ Reduction
Fig. 7. Iso-recursive Subtyping syntax_ott.v $\Sigma \vdash A \leq_{i} B $ AmberSubtyping
Fig. 7. Equi-recursive Subtyping syntax_ott.v $\Sigma \vdash A \leq_{e} B $ ACSubtyping

Note, in the formalization of the rules in literature (e.g. Brandt and Henglein's equi-recursive type equality in Fig. 2, Iso-recursive Subtyping, and Equi-recursive Subtyping in Fig. 7), we add a type context and well-formedness check to the rules in order to be consistent with the rest of the rules. The well-formedness conditions are omitted in the paper for simplicity.

Paper to Proof Table

The main system

Contains the proofs for the main system presented in Section 3 and Section 4 of the paper.

The paper to proof table:

Theorem File Name in Coq
Theorem 3.1 Soundness of Type Casting theorems.v TypCast_soundness
Theorem 3.1 Completeness of Type Casting theorems.v TypCast_completeness
Theorem 3.2 Equivalence of Alternative equi-recursive typing theorems.v equi_alt_equiv
Theorem 3.3 Equi-recursive to full iso-recursive typing theorems.v EquiTypingC_sem
Theorem 3.4 Full iso-recursive to equi-recursive typing theorems.v typing_i2e
Theorem 3.5 Round-tripping of the encoding theorems.v erase_typing
Theorem 3.6 Progress Progress.v progress
Theorem 3.7 Preservation Preservation.v preservation
Theorem 3.8 Full iso-recursive to equi-recursive reduction theorems.v reductions_i2e
Theorem 3.9 Behavioral equivalence theorems.v behavior_equiv

The subtyping system

Contains the proofs for the main system extended with subtyping presented in Section 5 of the paper.

The paper to proof table:

Theorem File Name in Coq
Theorem 5.1 Reflxixivty of Iso-recursive Subtyping subtyping.v AmberWFT_refl
Theorem 5.2 Transitivity of Iso-recursive Subtyping subtyping.v AmberSub_trans
Lemma 5.3 Unfolding Lemma subtyping.v unfolding_lemma
Theorem 5.4(1) Progress Progress.v progress
Theorem 5.4(2) Preservation Preservation.v preservation
Theorem 5.5 Equi-recursive subtyping decomposition theorems.v subtyping_decomposition
Theorem 5.6(1) Typing Equivalence - soundness theorems.v typing_i2e
Theorem 5.6(2) Typing Equivalence - completeness theorems.v EquiTypingC_sem
Theorem 5.6(3) Typing Equivalence - round-tripping theorems.v erase_typing
Theorem 5.7 Behavioral Equivalence theorems.v behavior_equiv