Mechanization accompanying the paper Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris, published at ICFP 2020.

The mapping between the paper and this mechanization, together with the layout of the codebase, is described in correspondence.md. See below for how to process sources with coqdoc.

We have also provided an artifact, matching our v1.0 release. Its instructions are in 00Artifact-README.md.

• GNU make
• opam 2.0.6 or later.

After the cloning, run

git submodule update --init --recursive

to fetch all git submodules.

The following commands will install the correct Coq version and the correct versions of the std++ and Iris libraries.

• If opam is not configured, run its setup wizard with opam init.
• Then, prepare for installation with:

eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released --set-default --all
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git --set-default --all
opam update

• If you use opam for other Coq projects, we recommend setting up a dedicated opam switch. Instructions appear in development.md.
• Actually install dependencies with:

opam install --deps-only .

Run make -jN to build the full development, where N is the number of your CPU cores; that should take around 5-10 minutes.

Start from here.

Run make html to run coqdoc over the code, to obtain an hyperlinked version (for ease of cross-referencing). html/toc.html offers an index for navigation; keep in mind that correspondence.md is a better overview.

See development.md.