\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 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 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 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:+ −