\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 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 of computation.  We
formalise Turing machines and relate them to abacus machines and
recursive functions. We also formalise a universal Turing machine and
Hoare-style reasoning techniques that allow us to reason about Turing machine
programs. Our theory can be used 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:
