--- a/Paper/Paper.thy	Thu Feb 07 05:32:00 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 05:46:17 2013 +0000
@@ -314,7 +314,7 @@
 \cite{AspertiRicciotti12}, instead follow the proof in
 \cite{Boolos87} by translating abacus machines to Turing machines and in
 turn recursive functions to abacus machines. The universal Turing
-machine can then be constructed as a recursive function.
+machine can then be constructed by translating from a recursive function. 
 
 \smallskip
 \noindent
@@ -330,7 +330,7 @@
 machines. This works essentially like a small, verified compiler 
 from recursive functions to Turing machine programs.
 When formalising the universal Turing machine,
-we stumbled upon an inconsistent use of the definition of
+we stumbled in \cite{Boolos87} upon an inconsistent use of the definition of
 what partial function a Turing machine calculates. 
 
 %Since we have set up in
@@ -508,13 +508,13 @@
   0}-state, but it will always perform a @{term Nop}-operation and
   remain in the @{text 0}-state.  Unlike Asperti and Riccioti
   \cite{AspertiRicciotti12}, we have chosen a very concrete
-  representation for programs, because when constructing a universal
+  representation for Turing machine programs, because when constructing a universal
   Turing machine, we need to define a coding function for programs.
   This can be directly done for our programs-as-lists, but is
   slightly more difficult for the functions used by Asperti and Ricciotti.
 
   Given a program @{term p}, a state
-  and the cell being read by the head, we need to fetch
+  and the cell being scanned by the head, we need to fetch
   the corresponding instruction from the program. For this we define 
   the function @{term fetch}
  
@@ -1561,15 +1561,15 @@
   undecidability of the halting problem for Turing machines.  This
   took us around 1500 loc of Isar-proofs, which is just one-and-a-half
   times of a mechanised proof pearl about the Myhill-Nerode
-  theorem. So our conclusion is that it not as daunting for this part of the
-  work as we estimated when reading the paper by Norrish \cite{Norrish11}. The work
+  theorem. So our conclusion is that this part is not as daunting 
+  as we estimated when reading the paper by Norrish \cite{Norrish11}. The work
   involved with constructing a universal Turing machine via recursive
   functions and abacus machines, we agree, is not a project
   one wants to undertake too many times (our formalisation of abacus
   machines and their correct translation is approximately 4300 loc;
   recursive functions 5000 loc and the universal Turing machine 10000 loc).
   
-  Our work was also very much inspired by the formalisation of Turing
+  Our work is also very much inspired by the formalisation of Turing
   machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the
   Matita theorem prover. It turns out that their notion of
   realisability and our Hoare-triples are very similar, however we
@@ -1581,7 +1581,7 @@
   infrastructure, we expect however this should not be too difficult 
   for them.
   
-  For us the most interesting aspect of our work are the correctness
+  For us the most interesting aspects of our work are the correctness
   proofs for Turing machines. Informal presentations of computability
   theory often leave the constructions of particular Turing machines
   as exercise to the reader, for example \cite{Boolos87}, deeming
@@ -1589,14 +1589,14 @@
   presentations leave out any arguments why these Turing machines
   should be correct.  This means the reader is left
   with the task of finding appropriate invariants and measures for
-  showing correctness and termination of these Turing machines.
+  showing the correctness and termination of these Turing machines.
   Whenever we can use Hoare-style reasoning, the invariants are
   relatively straightforward and much smaller than for example the
   invariants used by Myreen in a correctness proof of a garbage collector
   written in machine code \cite[Page 76]{Myreen09}. However, the invariant 
   needed for the abacus proof, where Hoare-style reasoning does not work, is
   similar in size as the one by Myreen and finding a sufficiently
-  strong one took us, like Myreen for his, something on the magnitude of
+  strong one took us, like Myreen, something on the magnitude of
   weeks.
 
   Our reasoning about the invariants is not much supported by the
@@ -1604,7 +1604,7 @@
   There is however a tantalising connection
   between our work and very recent work \cite{Jensen13} on verifying
   X86 assembly code that might change that. They observed a similar phenomenon with assembly
-  programs that Hoare-style reasoning is sometimes possible, but
+  programs where Hoare-style reasoning is sometimes possible, but
   sometimes it is not. In order to ease their reasoning, they
   introduced a more primitive specification logic, on which
   Hoare-rules can be provided for special cases.  It remains to be

Binary file paper.pdf has changed