37 \title{A Formalised Theorey about Turing Machines in Isablle/HOL}

    37 \title{A Formalised Theory of Turing Machines in Isabelle/HOL}

    40 \author{\IEEEauthorblockN{Authors Name/s per 1st Affiliation (Author)}

    40 \author{

    41 \IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\

    41 \IEEEauthorblockN{Xu Jian, Xingyuan Zhang}

    42 line 2: name of organization, acronyms acceptable\\

    42 \IEEEauthorblockA{PLA University of Science and Technology Nanjing, China}

    43 line 3: City, Country\\

    44 line 4: Email: name@xyz.com}

    46 \IEEEauthorblockN{Authors Name/s per 2nd Affiliation (Author)}

    44 \IEEEauthorblockN{Christian Urban}

    47 \IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\

    45 \IEEEauthorblockA{King's College London, UK}

    48 line 2: name of organization, acronyms acceptable\\

    49 line 3: City, Country\\

    50 line 4: Email: name@xyz.com}

    57 

    52 Isabelle/HOL is an interactive theorem prover based on classical 

    58 The abstract goes here. DO NOT USE SPECIAL CHARACTERS, SYMBOLS, OR MATH IN YOUR TITLE OR ABSTRACT.

    53 logic. While classical reasoning allow users to take convenient 

    54 shortcuts in some proofs, it precludes \emph{direct} reasoning about 

    55 decidability: every boolean predicate is either true or false

    56 because of the law of excluded middle. The only way to reason

    57 about decidability in a classical theorem prover, like Isabelle/HOL,

    58 is to formalise a concrete model for computation. In this paper

    59 we formalise Turing machines and relate them to register machines.