13 We formalised in earlier work the correctness 

    13 \noindent

    14 proofs for two algorithms in Isabelle/HOL, one about type-checking in LF and 

    14 We formalised in earlier work the correctness proofs for two

    15 another about deciding requests in access control \cite{UrbanCheneyBerghofer11} [???]: 

    15 algorithms in Isabelle/HOL---one about type-checking in

    16 these 

    16 LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests

    17 formalisations uncovered a gap in the informal correctness 

    17 in access control~\cite{WuZhangUrban12}.  The formalisations

    18 proof of the former and made us realise that important details 

    18 uncovered a gap in the informal correctness proof of the former and

    19 were left out in the informal model for the latter. However, 

    19 made us realise that important details were left out in the informal

    20 in both cases we were unable to formalise computablility 

    20 model for the latter. However, in both cases we were unable to

    21 arguments for the algorithms. The reason is that both algorithms are formulated

    21 formalise in Isabelle/HOL computability arguments about the

    22 in terms of inductive predicates. Suppose @{text "P"} stands for one such predicate.

    22 algorithms. The reason is that both algorithms are formulated in terms

    23 Decidability of @{text P} usually amounts to showing whether 

    23 of inductive predicates. Suppose @{text "P"} stands for one such

    24 @{term "P \<or> \<not>P"} holds. But this does not work in Isabelle/HOL,

    24 predicate.  Decidability of @{text P} usually amounts to showing

    25 since it is a theorem prover based on classical logic where

    25 whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work

    26 the law of excluded midle ensures that @{term "P \<or> \<not>P"} is 

    26 in Isabelle/HOL, since it is a theorem prover based on classical logic

    27 always provable.   

    27 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}

    28 is always provable no matter whether @{text P} is constructed by

    29 computable means. The same problem would arise if we had formulated

    30 the algorithms as recursive functions, because internally in

    31 Isabelle/HOL, like in all HOL-based theorem provers, functions are

    32 represented as inductively defined predicates.

    33 

    34 The only satisfying way out is to formalise a theory of

    35 computability. Norrish provided such a formalisation for the HOL4

    36 theorem prover. He choose the $\lambda$-calculus as the starting point

    37 for his formalisation, because of its ``simplicity'' \cite[Page

    38 297]{Norrish11}.  Part of his formalisation is a clever infrastructure

    39 for reducing $\lambda$-terms. He also established the computational

    40 equivalence between the lambda-calculus and recursive functions.

    41 Nevertheless he concluded that it would be appealing to have

    42 formalisations of more operational models of computations such as

    43 Turing machines or register machines.  One reason is that many proofs

    44 in the literature refer to them.  He noted however that in the context

    45 of theorem provers \cite[Page 310]{Norrish11}:

    46 

    47 \begin{quote}

    48 \it``If register machines are unappealing because of their 

    49 general fiddliness, Turing machines are an even more 

    50 daunting prospect.''

    51 \end{quote}

    52 

    53 \noindent

    54 In this paper 

    36 

    60 \cite{AspertiRicciotti12}

    37 Norrish choose the $\lambda$-calculus as a starting point

    38 for his formalisation, because of its ``simplicity'' [Norrish]

    39  

    40 ``Turing machines are an even more daunting prospect'' [Norrish]