Artifact POPL21 - Fully Abstract from Static to Gradual

The artifact accompanying the POPL21 paper titled "Fully Abstract from Static to Gradual" can be inspected in three ways. 1) The github repository containing the Coq proof can be found at https://github.com/scaup/fae-gtlc-mu. In its README.md file, one can find the following: The requirements to compile the Coq code How one can install these requirements Documentation explaining where one can find the relevant definitions and proofs with references to the paper. 2) A VM file (compatible with VirtualBox) can also be downloaded. It contains a copy of the aforementioned git repo (/home/username/fae-gtlc-mu), and it has the required version of Coq and the necessary libraries preinstalled. The VM also contains CoqIDE (linked on the dekstop), a gui to interact with the Coq code. The Coq files are already compiled; to recompile from scratch, one can do successively run 'make clean' and 'make' in the directory. 3) A zip file can also be downloaded. It contains a collection of clickable html files generated by coqdoc. One can start by looking at the overview.html file; it provides the same documentation as the README.md file of the aforementioned git repository