The proof is divided into the following files:
null.ott: Definitions of syntax and typing rules, corresponding to Figures 1-4, 6-7, and 9-11 in the paper. The Coq files Definitions.v and Infrastructure.v are mechanically generated from these definitions by ott and lngen, respectively.
Safety.v, pretty-printed in html/Safety.html: Lemmas in Section 3.1 of the paper.
Blame.v, pretty-printed in html/Blame.html: Definitions and lemmas in Sections 3.2 and 3.3 of the paper, including the definition of Safe Terms in Figure 5.
Desugaring.v, pretty-printed in html/Desugaring.html: Definitions and lemmas in Sections 4.3, 4.4, 5.1, 5.2, and 5.3 of the paper, including the definitions in Figure 8.
Running the Coq proofs requires the following dependencies installed using the specified versions of their opam packages:
coq 8.11.2
ott 0.31
coq-ott 0.31
It also requires lngen, installed as follows: 1) Install stack:
https://docs.haskellstack.org/en/stable/ 2) Build lngen from source:
git clone https://github.com/plclub/lngen.git cd lngen stack setup stack install
It also requires metalib, installed following the instructions at: https://github.com/plclub/metalib
With the above dependencies, the following commands build the proofs.
make
Runs Coq on all the proof files, without
running ott and lngen to regenerate Definitions.v and Infrastructure.v
from null.ott.
make doc
Pretty-prints the Coq source files in the
html subdirectory.
make all
Runs ott and lngen to regenerate
Definitions.v and Infrastructure.v from null.ott, runs Coq on all the
proof files, and pretty-prints the Coq source files in the html
directory.