This repository contains the accompanying Coq code for the above mentioned paper by Yannick Forster and Kathrin Stark, accepted for publication at CPP '20. The paper is avaiable here.
Parts of the Coq code were created using Autosubst 2. The directory metacoq contains a development version of MetaCoq.
Our development is tested under Coq 8.9.1 with the Equations package 1.2+8.9 (see below on how to install).
You need a development version of MetaCoq, which is contained in this zip file as well. Everything is handled by the Makefile and you can just type make.
If you need to install Coq first, make sure you have opam 2 installed and set up. You can then type
# opam switch create coq.8.9.1 4.07.1
# eval $(opam env)
# opam pin add coq 8.9.1
# opam pin add coq-equations 1.2+8.9to install Coq and the Equations package.