--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/root.tex	Sat Jul 27 08:17:54 2013 +0200
@@ -0,0 +1,86 @@
+\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: