\documentclass[runningheads]{llncs}%\documentclass[10pt, conference, compsocconf]{IEEEtran}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{times}\usepackage{amssymb}\usepackage{amsmath}\usepackage{mathpartir}\usepackage{pdfsetup}\usepackage{tikz}\usepackage{pgf}% urls in roman style, theory text in math-similar italics\urlstyle{rm}\isabellestyle{it}% 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{Formalising 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 prover Isabelle/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 for computation. We formalise Turing machines and relate them to abacus machines and recursivefunctions. Our theory can be used to formalise other computability results:{\it we give one example about the undecidability of Wang's tiling problem, whose proof usesthe 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: