\documentclass[10pt, conference, compsocconf]{IEEEtran}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage{times}

\usepackage{amssymb}

\usepackage{amsmath}

\usepackage{mathpartir}

\usepackage{pdfsetup}

\usepackage{tikz}

\usepackage{pgf}

% 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}{}

\begin{document}

\title{Formalising Computability Theory in Isabelle/HOL}

\author{

\IEEEauthorblockN{Jian Xu, Xingyuan Zhang}

\IEEEauthorblockA{PLA University of Science and Technology Nanjing, China}

\and

\IEEEauthorblockN{Christian Urban}

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

we give one example about the undecidability of Wang's tiling problem, whose proof uses

the notion of a universal Turing machine.

\end{abstract}

\begin{IEEEkeywords}

Turing Machines, Computability, Isabelle/HOL, Wang tilings

\end{IEEEkeywords}

\IEEEpeerreviewmaketitle

% generated text of all theories

\input{session}

% optional bibliography

\bibliographystyle{abbrv}

\bibliography{root}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: