Verified Programming of Turing Machines in Coq

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.

How to build

Required packages

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

Build external libraries

The Undecidability libraries depends on several external libraries. Initialise and build them once as follows:

git submodule init
git submodule update
make deps

Building the undecidability library

• make all builds the library
• make html generates clickable coqdoc .html in the website subdirectory
• make clean removes all build files in theories and .html files in the website directory
• make realclean also removes all build files in the external directory. You have to run make deps again after this.