1 \documentclass[runningheads]{llncs}

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

     3 \usepackage{isabelle}

     4 \usepackage{isabellesym}

     5 \usepackage{times}

     6 \usepackage{amssymb}

     7 \usepackage{amsmath}

     8 \usepackage{stmaryrd}

     9 \usepackage{mathpartir}

    10 \usepackage{pdfsetup}

    11 \usepackage{tikz}

    12 \usepackage{pgf}

    13 \usepackage{color}

    14 

    15 %% for testing

    16 %\usepackage{endnotes}

    17 %\let\footnote=\endnote

    18 

    19 % urls in roman style, theory text in math-similar italics

    20 \urlstyle{rm}

    21 \isabellestyle{it}

    22 

    23 % gray boxes

    24 \definecolor{mygrey}{rgb}{.80,.80,.80}

    25 

    26 % mathpatir

    27 \mprset{sep=0.9em}

    28 \mprset{center=false}

    29 \mprset{flushleft=true}

    30 

    31 % for uniform font size

    32 %\renewcommand{\isastyle}{\isastyleminor}

    33 

    34 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    35 \renewcommand{\isasymequiv}{$\dn$}

    36 \renewcommand{\isasymemptyset}{$\varnothing$}

    37 \renewcommand{\isacharunderscore}{\mbox{$\_$}}

    38 \renewcommand{\isasymiota}{}

    39 \newcommand{\isasymulcorner}{$\ulcorner$}

    40 \newcommand{\isasymurcorner}{$\urcorner$}

    41 \begin{document}

    42 

    43 

    44 \title{Mechanising Turing Machines and Computability Theory in Isabelle/HOL}

    45 \author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}

    46 \institute{PLA University of Science and Technology, China \and King's College London, UK}

    47 

    48 \maketitle

    49 

    50 

    51 \begin{abstract}

    52 We formalise results from computability theory in the theorem prover

    53 Isabelle/HOL. 

    54 %This theorem prover is based on classical logic which

    55 %precludes \emph{direct} reasoning about computability: every boolean

    56 %predicate is either true or false because of the law of excluded

    57 %middle. The only way to reason about computability in a classical

    58 %theorem prover is to formalise a concrete model of computation.  

    59 Following the textbook by Boolos et al, we formalise Turing machines

    60 and relate them to abacus machines and recursive functions. We ``tie

    61 the know'' between these three computational models by formalising a

    62 universal function and obtaining from it a universal Turing machine by

    63 our verified translation from recursive functions to abacus programs

    64 and from abacus programs to Turing machine programs.  Hoare-style reasoning techniques allow us

    65 to reason about concrete Turing machine and abacus programs. 

    66 %Our theory can be

    67 %used to formalise other computability results.

    68 %We give one example about the computational equivalence of 

    69 %single-sided Turing machines. 

    70 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses

    71 %the notion of a universal Turing machine.}

    72 \end{abstract}

    73 

    74 % generated text of all theories

    75 \input{session}

    76 

    77 % optional bibliography

    78 \bibliographystyle{abbrv}

    79 \bibliography{root}

    80 

    81 \end{document}

    82 

    83 %%% Local Variables:

    84 %%% mode: latex

    85 %%% TeX-master: t

    86 %%% End: