\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 formalise results from computability theory 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.  

Following the textbook by Boolos et al, we formalise Turing machines

and relate them to abacus machines and recursive functions. We ``tie

the know'' between these three computational models by formalising a

universal function and obtaining from it a universal Turing machine by

our verified translation from recursive functions to abacus programs

and from abacus programs to Turing machine programs.  Hoare-style reasoning techniques allow us

to reason about concrete Turing machine and abacus 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: