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 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.
A Formalization of Multi-tape Turing Machines
A. Asperti, W. Ricciotti
Initial Seminar Talk: Comming soon (21th Dezember 2017)
Thu Dec 14 22:22:53 2017