--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.tex	Fri Jan 18 11:40:01 2013 +0000
@@ -0,0 +1,62 @@
+\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}
+
+% 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{Formalising 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: