\documentclass[runningheads]{llncs}%\documentclass[10pt, conference, compsocconf]{IEEEtran}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{times}\usepackage{amssymb}\usepackage{amsmath}\usepackage{stmaryrd}\usepackage{mathpartir}\usepackage{pdfsetup}\usepackage{tikz}\usepackage{pgf}\usepackage{color}%% for testing%\usepackage{endnotes}%\let\footnote=\endnote% urls in roman style, theory text in math-similar italics\urlstyle{rm}\isabellestyle{it}% gray boxes\definecolor{mygrey}{rgb}{.80,.80,.80}% mathpatir\mprset{sep=0.9em}\mprset{center=false}\mprset{flushleft=true}% for uniform font size%\renewcommand{\isastyle}{\isastyleminor}\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}\renewcommand{\isasymequiv}{$\dn$}\renewcommand{\isasymemptyset}{$\varnothing$}\renewcommand{\isacharunderscore}{\mbox{$\_$}}\renewcommand{\isasymiota}{}\newcommand{\isasymulcorner}{$\ulcorner$}\newcommand{\isasymurcorner}{$\urcorner$}\begin{document}\title{Mechanising Turing Machines and Computability Theory in Isabelle/HOL}\author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}\institute{PLA University of Science and Technology, China \and King's College London, UK}\maketitle\begin{abstract}We present a formalised theory of computability in the theorem proverIsabelle/HOL. %This theorem prover is based on classical logic which%precludes \emph{direct} reasoning about computability: every boolean%predicate is either true or false because of the law of excluded%middle. The only way to reason about computability in a classical%theorem prover is to formalise a concrete model of computation. Following the textbook by Boolos et al, we formalise Turing machinesand relate them to abacus machines and recursive functions. We ``tiethe know'' between these three computational models by formalising auniversal function and obtaining from it a universal Turing machine byour verified translation from recursive functions to abacus programsand from abacus programs to Turing machine programs. Hoare-style reasoning techniques allow usto reason about Turing machine and abacus programs. Our theory can beused to formalise other computability results.%We give one example about the computational equivalence of %single-sided Turing machines. %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses%the notion of a universal Turing machine.}\end{abstract}% generated text of all theories\input{session}% optional bibliography\bibliographystyle{abbrv}\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: