Maximilian Wuttke: Bachelor's Thesis

Saarland University Computer Science

Formalizing 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. Finally, we introduce a class of encoding predicates and define what it means that a machine calculates a function. Our goal is to work towards the verification of a multi-tape Turing machine that can simulate the weak call-by-value lambda calculus L.



Initial Seminar Talk: Comming soon (21th Dezember 2017)

Maximilian Wuttke, Fri Dec 15 13:23:47 2017