Description
Coq development of theorems and proofs for the paper: "Contextual Equivalence for a Language with Continuous Random Variables and Recursion" by Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb (ICFP 2018, https://doi.org/10.1145/3236782).
Assets
Instructions
General Installation
Software Dependencies:
- Coq 8.6 (also tested with Coq 8.8) - [Autosubst](https://github.com/uds-psl/autosubst) (use the `coq86-devel` branch) - [Coquelicot](http://coquelicot.saclay.inria.fr/)
General Installation:
On a fresh Ubuntu 18.04 system, the following steps are sufficient to install Coq and the libraries that our code depends on. - install coq and coquelicot via opam: - `sudo apt install build-essential git opam m4` - `opam init --auto-setup` - ```eval `opam config env` ``` - `opam repo add coq-released http://coq.inria.fr/opam/released` - `opam install coq.8.8.0 coq-coquelicot.3.0.2` - Note: this step might fail on machines with less than 3 GB memory. - This also installs `coq-mathcomp-ssreflect.1.7.0`, a dependency of Coquelicot. - check out, build, and install autosubst: - `git clone -b coq86-devel https://github.com/uds-psl/autosubst.git` - The head commit of branch coq86-devel was d0d7355797. - `pushd autosubst` - `make` - This may print warnings: "fix/cofix without a name are deprecated...". These warnings may be ignored. - `make install` - `popd` - compile our coq development: - `make`
Provenance
This material is based upon work sponsored by the Air Force Research Laboratory (AFRL) and the Defense Advanced Research Projects Agency (DARPA) under Contract No. FA8750-14-C-0002. The views expressed are those of the authors and do not reflect the official policy or position of the Department of Defense or the U.S. Government.
