Mechanising Turing Machines and Computability Theory in Isabelle/HOL

Abstract. We formalise results from computability theory in the theorem prover Isabelle/HOL. Following the textbook by Boolos et al, we formalise Turing ma-chines and relate them to abacus machines and recursive functions. We “tie the knot ” between these three computational models by formalising a universal func-tion and obtaining from it a universal Turing machine by our verified translation from recursive functions to abacus programs and from abacus programs to Tur-ing machine programs. Hoare-style reasoning techniques allow us to reason about concrete Turing machine and abacus programs.