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