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 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, 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 it to build and certify a multi-tape Turing machine that can simulate the week call-by-value lambda calculus L.



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

Maximilian Wuttke, Thu Dec 14 22:22:53 2017