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. The GitHub repo is here.
Coq 8.7 or 8.8 or 8.9 is required.
Get the source code and the libraries via
git clone https://github.com/uds-psl/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 are taken from Asperti, Riciotti "A formalization of multi-tape Turing machines" (2015) and the accompanying Matita mechanisation.
My advisor of this thesis, Yannick Forster, did the initial translation from Matita to Coq and implemented some prototypes.
Please also read the Acknowledgements section of 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 located inside tex/thesis.
It can be built using make.
It can be downloaded from here.
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, but excluding the external libraries) are Copyright(c) 2017-2018 Maximilian Wuttke.