--- a/Paper.thy	Sun Dec 30 14:58:48 2012 +0000
+++ b/Paper.thy	Sun Dec 30 21:18:39 2012 +0000
@@ -10,34 +10,54 @@
 
 text {*
 
-We formalised in earlier work the correctness 
-proofs for two algorithms in Isabelle/HOL, one about type-checking in LF and 
-another about deciding requests in access control \cite{UrbanCheneyBerghofer11} [???]: 
-these 
-formalisations uncovered a gap in the informal correctness 
-proof of the former and made us realise that important details 
-were left out in the informal model for the latter. However, 
-in both cases we were unable to formalise computablility 
-arguments for the algorithms. The reason is that both algorithms are formulated
-in terms of inductive predicates. Suppose @{text "P"} stands for one such predicate.
-Decidability of @{text P} usually amounts to showing whether 
-@{term "P \<or> \<not>P"} holds. But this does not work in Isabelle/HOL,
-since it is a theorem prover based on classical logic where
-the law of excluded midle ensures that @{term "P \<or> \<not>P"} is 
-always provable.   
+\noindent
+We formalised in earlier work the correctness proofs for two
+algorithms in Isabelle/HOL---one about type-checking in
+LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests
+in access control~\cite{WuZhangUrban12}.  The formalisations
+uncovered a gap in the informal correctness proof of the former and
+made us realise that important details were left out in the informal
+model for the latter. However, in both cases we were unable to
+formalise in Isabelle/HOL computability arguments about the
+algorithms. The reason is that both algorithms are formulated in terms
+of inductive predicates. Suppose @{text "P"} stands for one such
+predicate.  Decidability of @{text P} usually amounts to showing
+whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work
+in Isabelle/HOL, since it is a theorem prover based on classical logic
+where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
+is always provable no matter whether @{text P} is constructed by
+computable means. The same problem would arise if we had formulated
+the algorithms as recursive functions, because internally in
+Isabelle/HOL, like in all HOL-based theorem provers, functions are
+represented as inductively defined predicates.
+
+The only satisfying way out is to formalise a theory of
+computability. Norrish provided such a formalisation for the HOL4
+theorem prover. He choose the $\lambda$-calculus as the starting point
+for his formalisation, because of its ``simplicity'' \cite[Page
+297]{Norrish11}.  Part of his formalisation is a clever infrastructure
+for reducing $\lambda$-terms. He also established the computational
+equivalence between the lambda-calculus and recursive functions.
+Nevertheless he concluded that it would be appealing to have
+formalisations of more operational models of computations such as
+Turing machines or register machines.  One reason is that many proofs
+in the literature refer to them.  He noted however that in the context
+of theorem provers \cite[Page 310]{Norrish11}:
+
+\begin{quote}
+\it``If register machines are unappealing because of their 
+general fiddliness, Turing machines are an even more 
+daunting prospect.''
+\end{quote}
+
+\noindent
+In this paper 
 
 
 
 
-These algorithms
-were given as inductively defined predicates.  
-inductively defined predicates, but 
 
-
-Norrish choose the $\lambda$-calculus as a starting point
-for his formalisation, because of its ``simplicity'' [Norrish]
- 
-``Turing machines are an even more daunting prospect'' [Norrish]
+\cite{AspertiRicciotti12}
 
 
 Our formalisation follows XXX