Maximilian Wuttke: Bachelor's Thesis

Saarland University Computer Science

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.



Maximilian Wuttke, Fri Mar 16 02:26:09 2018