This repository accompanies the paper Verified Programming of Turing Machines in Coq by Yannick Forster, Fabian Kunze, and Maximilian Wuttke, which appeared at the CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. The paper can also be found here.
The repository is a static fork of the Coq Library of Undecidability Proofs.
You need Coq 8.8.1 or 8.8.2 built on OCAML > 4.02.3 and the Equations package for Coq. If you’re using opam 2 you can use the following commands to install the dependencies on a new switch:
opam switch create coq-library-undecidability 4.07.1+flambda
eval $(opam env)
opam install . --deps-only
The Undecidability libraries depends on several external libraries. Initialise and build them once as follows:
git submodule init
git submodule update
make deps
make all builds the librarymake html generates clickable coqdoc .html in the website subdirectorymake clean removes all build files in theories and .html files in the website directorymake realclean also removes all build files in the external directory. You have to run make deps again after this.