Maximilian Wuttke's Bachelor's Thesis at the Programming Sytems Lab at Saarland University.

The project's home page is here.

The online CoqDoc can be found here.

Coq 8.7 or 8.8 is required.

Get the source code and the libraries via

git clone https://github.com/mwuttke97/CoqTM
cd CoqTM
git submodule update --init --recursive

Compile the libraries:

cd external/base && make -j
cd ../smpl && make -j
cd ../..

Note that if you have Coq 8.7, you need to execute git checkout v8.7 inside external/smpl. Compile the main source code:

make -j

This should take ca. 5-10 minutes.

The definitions of tapes and multi-tape Turing machines from Asperti, Riciotti "A formalization of multi-tape Turing machines" (2015) and the accompanying Matita mechanisation. Please also read the Acknowledgements section inside the thesis.

This project uses two libraries:

• Base Library: Coq library for finite types, retracts, and inhabited types
• smpl: A Coq plugin providing an extensible tactic similar to first.

Please consult the README files in the corresponding repos; the links are found under externals/.

We use CoqDocJS to make the CoqDoc code a bit fancier.

The source code of the thesis is found inside tex/thesis. It can be built using make.

The source code is Copyright(c) 2017-2018 Maximilian Wuttke. It is licensed under the MIT License.

All other files (including the thesis and its source code) are Copyright(c) 2017-2018 Maximilian Wuttke.