\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 whichprecludes \emph{direct} reasoning about computability: every booleanpredicate is either true or false because of the law of excludedmiddle. The only way to reason about computability in a classicaltheorem prover is to formalise a concrete model of computation. Weformalise Turing machines and relate them to abacus machines andrecursive functions. We also formalise a universal Turing machine andHoare-style reasoning techniques that allow us to reason about Turing machineprograms. Our theory can be used to formalise other computabilityresults. 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: