Maximilian Wuttke: Bachelor's Thesis
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.
A Formalization of Multi-tape Turing Machines
A. Asperti, W. Ricciotti
Initial Seminar Talk: Comming soon (21th Dezember 2017)
Fri Dec 15 13:23:47 2017