Welcome to the homepage of our paper, Undecidability of D<: and Its Decidable Fragments!
The paper has been put available on ACM Digital Library!
There are three ways to examine our artifact:
The easiest way is to simply run the Ubuntu VM!
It is also possible to build from our source. The binary dependencies are
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/
agda2.5.4.2 Everything.agda
or by loading from Emacs.
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 axiomfree, predicative and purely constructive.
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.The entry point is Everything.agda. The structure of the files are explained there.
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 stareat subtyping and examines its properties.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<:′ 
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 
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 
To make formalization work, there are proof engineering details that are not exposed in the paper. They include:
D<:
belong to this category.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.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′
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 coq8.8.2 4.05.0
eval $(opam env)
opam pin add coq 8.8.2
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 release2.5.4.2
cp stack8.4.4.yaml stack.yaml
stack stall # it is going to take a while
cp ~/.local/bin/agda ~/.local/bin/agda2.5.4.2
cp ~/.local/bin/agdamode ~/.local/bin/agdamode2.5.4.2