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

%% for testing

\usepackage{endnotes}

\let\footnote=\endnote

% 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{Mechanising 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. 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 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: