Undecidability of D<: and Its Decidable Fragments

Welcome to the homepage of our paper, Undecidability of D<: and Its Decidable Fragments!

The paper has been put available on ACM Digital Library!

The Artifact

There are three ways to examine our artifact:

download and run our VirtualBox VM,
clone our Github repository, or
directly download our artifact package.

The easiest way is to simply run the Ubuntu VM!

It is also possible to build from our source. The binary dependencies are

Coq 8.8.2
Agda 2.5.4.2

Library dependencies are in lib/ folder, which will be built automatically.

For a recommended way to installing Coq and Agda, please refer to the end of this page.

Dependencies are automatically built by

make -B

This command will also build dsub/ folder which contains the Coq proofs.

We use git's submodules and if one pulls our repo, the submodules are not automatically pulled. make should ensure those modules exist before building. In case unexpected event occurs, one could update submodules by

git submodule init
git submodule update

fsub/ folder can be built by

make fsub

The Agda proofs can be verified by

cd agda/
agda-2.5.4.2 Everything.agda

or by loading from Emacs.

Correspondence Between The Paper and Formalization

The formalization is done with a combination of Agda and Coq. The undecidability proofs are done in Agda (section 4) and the proofs of algorimic subtyping are done in Coq (section 5 and 6).

The formalization is axiom-free, predicative and purely constructive.

Folder structure

The artifact consists of the following folders.

agda/ contains the undecidability proofs in Agda.
fsub/ contains the proofs of algorithmic subtyping of F<: in Coq.
dsub/ contains the proofs of algorithmic subtyping of D<: in Coq.
lib/ contains external dependencies.
share/ contains library specifically designed for this project.

Structure of Agda Proofs

The entry point is Everything.agda. The structure of the files are explained there.

Structure of Coq Proofs

There are Coq proofs in fsub/ and dsub/, and the proofs are organized in the following ways:

Definition.v defines the abstract syntax and judgments of the calculus.
OperationProperties.v, StructuralProperties.v and Misc.v include necessary technical setup.
OpeSub.v defines OPE<: and verifies its properties.
StrongKernel.v defines and verifies the properties of strong kernel.

In dsub/, there are following additional files:

Kernel.v defines kernel D<: and examines its properties.
Step.v defines step subtyping and examines its properties.
Stareat.v defines stare-at subtyping and examines its properties.

The undecidability proofs

The paper made brief discussion on why F<:- is undecidable. In the Agda proof, this is justified by reducing from F<: deterministic, F<:d, to F<:-. F<:d is an intermediate calculus in Pierce92, which was shown reducible from TCM, and therefore F<:d is undecidable as well as F<:-.

Theorem	File	Related Formalization
2	DsubFull.agda	`<:⇒<:′` and `<:′⇒<:`
5	FsubMinus.agda	`minus⇒deterministic` and `deterministic⇒minus`
6	DsubDef.agda	`contraInvertible`
	DsubReduced.agda	`⟪⟫-contraEnv`
7, 8, 9	DsubDef.agda	under `module InvertibleProperties`, and
	Dsub.agda	`module DsubInvProperties`
10	DsubEquivSimpler.agda	under `module SimplerTransitivity`
11	DsubEquivSimpler.agda	`<:⇒<:″` and `<:″⇒<:`
12, 13	DsubEquivSimpler.agda	`F<:⇒D<:` and `D<:⇒F<:`
14	DsubNoTrans.agda	`F<:⇒D<:` and `D<:⇒F<:`
15, 16	DsubTermUndec.agda	`F<:⇒typing′` and `typing⇒F<:′`

Kernel D<: and Step subtyping

Theorem	File	Related Formalization
17	Kernel.v	`subtykn_sound`
18	Step.v	`stp_subty_sound`
19	Step.v	`stp_subty_terminates`
20	Kernel.v	`subtykn_refl`
21	Kernel.v	`trans_on_top`
22	Kernel.v	`trans_on_bot`
23	Kernel.v	`exposure'_to_subtykn`
	Step.v	`exposure_to_exposure'`, `exposure'_to_exposure`
24	Kernel.v	`stp_subty_to_subtykn`
25	Kernel.v	`subtykn_to_stp_subty`, `subtykn_to_stp_subty'`, `stp_subty'_to_stp_subty`, `subtykn'_conversions`
	Step.v	`exposure_strengthening`

Strong Kernel D<: and Stare-at subtyping

Theorem	File	Related Formalization
26	StrongKernel.v	`subtysk_refl`
27	StrongKernel.v	`subtykn_to_subtysk`
28	StrongKernel.v	`subtysk_sound`
29	OpeSub.v	`ope_sub_refl`
30	OpeSub.v	`ope_sub_trans`
31	OpeSub.v	`ope_narrow_subty`
32	StrongKernel.v	`subtysk_sound_gen`
33	Step.v	`revealing_gives_prefix`
34, 35	Stareat.v	`revealing_sound`
36	Stareat.v	`revealing_preserves_wf`
37	Stareat.v	`upcast_sound`, `upcast_preserves_wf`, `downcast_sound`, `downcast_preserves_wf`
	Step.v	`upcast_gives_prefix`, `downcast_gives_prefix`
38	Stareat.v	`ope_sub_stareat_sound`
39	Stareat.v	`bsubtyp_sound`
40	Stareat.v	`revealing_terminates`
41	Stareat.v	`revealing_measure`, `upcast_decreases_measure`, and `downcast_decreases_measure`
42	Stareat.v	`stareat_terminates`
43	StrongKernel.v	`revealing_to_subtysk`, `exposure'_to_subtysk`
44	StrongKernel.v	`stareat_to_subtysk`, `stareat'_to_subtysk`, `stareat_to_stareat'`
45	Step.v	`stareat_strengthening`
46	StrongKernel.v	`subtysk_to_stareat`, `subtysk_to_stareat'`, `stareat'_to_stareat`, `subtysk'_conversions`

Strong Kernel and Stare-at Subtyping in F<:

In Secion 7, we discuss how to adapt our methods in F<:, and we also formalized this part in fsub/.

Theorem	File	Related Formalization
47	StrongKernel.v	`k_subty_to_sk_subty`
48	StrongKernel.v	`sk_subty_sound`
49	StrongKernel.v	`stareat_sound`
50	StrongKernel.v	`stareat_to_sk_subty`
51	StrongKernel.v	`sk_subty_to_stareat`
52	StrongKernel.v	`stareat_terminates`

Proof engineering

To make formalization work, there are proof engineering details that are not exposed in the paper. They include:

In Agda, names are modelled using De Bruijn indices.
In Coq, names are modelled using locally nameless representation with cofinite quantification. Therefore, in addition to requiring a type being closed w.r.t. the context, well-formedness condition also requires that the types are locally closed.
Some conclusions in the formalization are results of equivalences of intermediate languages which are not mentioned in the paper. For example, completeness theorems of kernel and strong kernel D<: belong to this category.
Step subtyping and Stare-at subtyping are modelled as program traces. In addition to every input/output, the relations also rely on a name store, very often represented by L, which means when a free name is drawn from a supply, the name must not be in L. This is a realistic treatment when free names are necessary in a program trace.
There are theorems in the paper which require to count the steps of derivation. In this case, separate relations are defined. Each of such relations copies its corresponding original relation, and additionally has a step counter, usually represented by n. Then this relation is shown to be equivalent to the original one. That is, if the original relation is R ⊆ X × Y, then define R′ ⊆ X × Y × ℕ, such that (x, y) ∈ R ⇔ ∃ n, (x, y, n) ∈ R′

Binary Installation

Installing Coq

Please ensure that all related binaries can be found in PATH. If a binary is not found, please check your PATH of your shell.

To install Coq, it is recommended to install via opam2, which can be installed via

sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

Then the following script will create a switch with the proper compiler version and install Coq.

opam switch create coq-8.8.2 4.05.0
eval $(opam env)
opam pin add coq 8.8.2

Installing Agda

It is recommended to build Agda from source. To do so, one would need to install stack. This can be done via

curl -sSL https://get.haskellstack.org/ | sh

Then the following script will use stack to install Agda in ~/.local/bin/.

git clone https://github.com/agda/agda
cd agda
git checkout release-2.5.4.2
cp stack-8.4.4.yaml stack.yaml
stack stall # it is going to take a while
cp ~/.local/bin/agda ~/.local/bin/agda-2.5.4.2
cp ~/.local/bin/agda-mode ~/.local/bin/agda-mode-2.5.4.2