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 while not using any axioms. To certify those machines we use a relational approach similar to Asperti et al. We make it concrete what it means that a machine behaves correctly by means that it realises a correctness relation. 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 it to build and certify a multitape Turing machine that can simulate the week 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,
Thu Dec 14 22:22:53 2017