The supplementary material contains three parts:
-
The formalized Coq proof, with pre-built documentation. Start by browsing the online documentation and/or
suppl-material/coqproof/Overview.v
.The formalization was last tested with Coq 8.8.1 and 8.8.2 and the Equations plugin version 1.1.
-
The evaluation case studies and benchmarks, including raw data. Start at
casestudy/README.md
.