--- 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

--- a/document/root.bib	Sun Dec 30 14:58:48 2012 +0000
+++ b/document/root.bib	Sun Dec 30 21:18:39 2012 +0000
@@ -7,3 +7,33 @@
   year = {2011},
   pages = {15:1--15:42}
 }
+
+@inproceedings{Norrish11,
+  author    = {M.~Norrish},
+  title     = {{M}echanised {C}omputability {T}heory},
+  booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving (ITP)},
+  year      = {2011},
+  series    = {LNCS},
+  volume    = {6898},
+  pages     = {297--311}
+}
+
+@inproceedings{AspertiRicciotti12,
+  author    = {A.~Asperti and W.~Ricciotti},
+  title     = {{F}ormalizing {T}uring {M}achines},
+  booktitle = {Proc.~of the 19th International Workshop on Logic, Language, 
+               Information and Computation (WoLLIC)},
+  year      = {2012},
+  pages     = {1-25},
+  series    = {LNCS},
+  volume    = {7456}
+}
+
+
+@Unpublished{WuZhangUrban12,
+  author = 	 {C.~Wu and X.~Zhang and C.~Urban},
+  title = 	 {???},
+  note = 	 {Submitted},
+  year = 	 {2012}
+}
+

--- a/document/root.tex	Sun Dec 30 14:58:48 2012 +0000
+++ b/document/root.tex	Sun Dec 30 21:18:39 2012 +0000
@@ -1,26 +1,8 @@
 \documentclass[10pt, conference, compsocconf]{IEEEtran}
-\usepackage{isabelle,isabellesym}
-
-%\usepackage{amssymb}
-  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
-  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
-  %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage[greek,english]{babel}
-  %option greek for \<euro>
-  %option english (default language) for \<guillemotleft>, \<guillemotright>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
-  %for \<Sqinter>
-
-%\usepackage{eufrak}
-  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
-  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
-  %\<currency>
-
-% this should be the last package used
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{times}
+\usepackage{amssymb}
 \usepackage{mathpartir}
 \usepackage{pdfsetup}
 
@@ -67,15 +49,6 @@
 
 \IEEEpeerreviewmaketitle
 
-
-%\tableofcontents
-
-% sane default for proof documents
-\parindent 0pt\parskip 0.5ex
-
-
-
-
 % generated text of all theories
 \input{session}
 

Binary file paper.pdf has changed