Maximilian Wuttke: Bachelor's Thesis
Formalising Multi-Tape Turing Machines
Advisor: Yannick Forster
We give a formalisation of multi-tape Turing machines in the proof assistant Coq. We make it concrete what it means that a machine is correct by using correctness relations following Asperti and Ricciotti. We implement basic machines and introduce building patterns like sequential composition, if-then-else, do-while, and match that can be used to easily build compound machines. Transformation operations can add new tapes or symbols, or can mirror the behaviour of a machine.
Initial Seminar Talk:
(21th Dezember 2017)
Fri Mar 16 02:26:09 2018