Maximilian Wuttke: Bachelor's Thesis
Formalizing Turing Machines
Advisor: Yannick Forster
Abstract:
We give a formalisation of multitape 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, ifthenelse, dowhile, 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 multitape Turing machine that can simulate the weak callbyvalue lambda calculus L.
References:

A Formalization of Multitape Turing Machines
(2013)
A. Asperti, W. Ricciotti
Downloads
Initial Seminar Talk: Comming soon (21th Dezember 2017)
Maximilian Wuttke,
Fri Dec 15 13:23:47 2017