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

     9 \usepackage{pdfsetup}

    10 \usepackage{tikz}

    11 \usepackage{pgf}

    12 

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

    14 \urlstyle{rm}

    15 \isabellestyle{it}

    16 

    17 % for uniform font size

    18 %\renewcommand{\isastyle}{\isastyleminor}

    19 

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

    21 \renewcommand{\isasymequiv}{$\dn$}

    22 \renewcommand{\isasymemptyset}{$\varnothing$}

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

    24 \renewcommand{\isasymiota}{}

    25 \newcommand{\isasymulcorner}{$\ulcorner$}

    26 \newcommand{\isasymurcorner}{$\urcorner$}

    27 \begin{document}

    28 

    29 

    30 \title{Formalising Computability Theory in Isabelle/HOL}

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

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

    33 

    34 \maketitle

    35 

    36 

    37 \begin{abstract}

    38 We present a formalised theory of computability in the 

    39 theorem prover Isabelle/HOL. This theorem prover is based on classical 

    40 logic which precludes \emph{direct} reasoning about computability: every 

    41 boolean predicate is either true or false because of the law of excluded 

    42 middle. The only way to reason about computability in a classical theorem 

    43 prover is to formalise a concrete model for computation. 

    44 We formalise Turing machines and relate them to abacus machines and recursive

    45 functions. Our theory can be used to formalise other computability results:

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

    47 the notion of a universal Turing machine.

    48 \end{abstract}

    49 

    50 % generated text of all theories

    51 \input{session}

    52 

    53 % optional bibliography

    54 \bibliographystyle{abbrv}

    55 \bibliography{root}

    56 

    57 \end{document}

    58 

    59 %%% Local Variables:

    60 %%% mode: latex

    61 %%% TeX-master: t

    62 %%% End: