\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}

%% for testing

\usepackage{endnotes}

\let\footnote=\endnote

% urls in roman style, theory text in math-similar italics

\urlstyle{rm}

\isabellestyle{it}

% mathpatir

\mprset{sep=0.8em}

\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 for computation.  We

formalise Turing machines and relate them to abacus machines and

recursive functions. We also formalise a universal Turing machine and

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: