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