Overview

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 Coq

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.