--- a/Paper/Paper.thy	Wed Jun 30 16:56:37 2010 +0100
+++ b/Paper/Paper.thy	Thu Jul 01 01:53:00 2010 +0100
@@ -853,7 +853,7 @@
   the definitions for $\alpha$-equivalence will help us in the next section.
 *}
 
-section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
+section {* Specifying General Binders\label{sec:spec} *}
 
 text {*
   Our choice of syntax for specifications is influenced by the existing
@@ -945,7 +945,7 @@
   of the specifications (the corresponding $\alpha$-equivalence will differ). We will 
   show this later with an example.
   
-  There are some restrictions we need to impose on binding clasues: the main idea behind 
+  There are some restrictions we need to impose on binding clauses: the main idea behind 
   these restrictions is that we obtain a sensible notion of $\alpha$-equivalence where
   it is ensured that a bound variable cannot be free at the same time.  First, a
   body can only occur in \emph{one} binding clause of a term constructor (this ensures
@@ -1121,7 +1121,11 @@
   \noindent 
   The point of completion is that we can make definitions over the binding
   clauses and be sure to have captured all arguments of a term constructor. 
+*}
 
+section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
+
+text {*
   Having dealt with all syntax matters, the problem now is how we can turn
   specifications into actual type definitions in Isabelle/HOL and then
   establish a reasoning infrastructure for them. As
@@ -1185,7 +1189,7 @@
   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
   that calculates those unbound atoms. 
 
-  For atomic types we define the auxilary
+  For atomic types we define the auxiliary
   free variable functions:
 
   \begin{center}
@@ -1285,7 +1289,7 @@
   \noindent
   Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}
   and @{text "ACons"}, the corresponding free-variable function @{text
-  "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The
+  "fv\<^bsub>assn\<^esub>"} returns all atoms occurring in an assignment. The
   binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
   "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
   @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
@@ -1915,7 +1919,7 @@
 section {* Related Work *}
 
 text {*
-  To our knowledge, the earliest usage of general binders in a theorem prover
+  To our knowledge the earliest usage of general binders in a theorem prover
   is described in \cite{NaraschewskiNipkow99} about a formalisation of the
   algorithm W. This formalisation implements binding in type schemes using a
   de-Bruijn indices representation. Since type schemes of W contain only a single
@@ -1926,7 +1930,7 @@
   of two numbers, one referring to the place where a variable is bound and the
   other to which variable is bound. The reasoning infrastructure for both
   representations of bindings comes for free in theorem provers like Isabelle/HOL or
-  Coq, as the corresponding term-calculi can be implemented as ``normal''
+  Coq, since the corresponding term-calculi can be implemented as ``normal''
   datatypes.  However, in both approaches it seems difficult to achieve our
   fine-grained control over the ``semantics'' of bindings (i.e.~whether the
   order of binders should matter, or vacuous binders should be taken into
@@ -1937,7 +1941,7 @@
   Another representation technique for binding is higher-order abstract syntax
   (HOAS), which for example is implemented in the Twelf system. This representation
   technique supports very elegantly many aspects of \emph{single} binding, and
-  impressive work is in progress that uses HOAS for mechanising the metatheory
+  impressive work has been done that uses HOAS for mechanising the metatheory
   of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
   binders of SML are represented in this work. Judging from the submitted
   Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
@@ -1948,7 +1952,7 @@
   all the unwanted consequences when reasoning about the resulting terms.
 
   Two formalisations involving general binders have also been performed in older
-  versions of Nominal Isabelle (one about Psi-calculi and one about alpgorithm W 
+  versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W 
   \cite{BengtsonParow09, UrbanNipkow09}).  Both
   use the approach based on iterated single binders. Our experience with
   the latter formalisation has been disappointing. The major pain arose from
@@ -2054,7 +2058,7 @@
   $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
   This definition is similar to the one by Pottier, except that it
   has a more operational flavour and calculates a partial (renaming) map. 
-  In this way they can handle vacous binders. However, their notion of
+  In this way they can handle vacuous binders. However, their notion of
   equality between terms also includes rules for $\beta$ and to our
   knowledge no concrete mathematical result concerning their notion
   of equality has been proved.    
@@ -2115,14 +2119,12 @@
   \medskip
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
-  many discussions about Nominal Isabelle. We thank Peter Sewell for 
+  many discussions about Nominal Isabelle. We also thank Peter Sewell for 
   making the informal notes \cite{SewellBestiary} available to us and 
-  also for patiently explaining some of the finer points of the work on the Ott-tool. We
-  also thank Stephanie Weirich for suggesting to separate the subgrammars
+  also for patiently explaining some of the finer points of the work on the Ott-tool.
+  Stephanie Weirich suggested to separate the subgrammars
   of kinds and types in our Core-Haskell example.  
 
-
-  * Conference of Altenkirch *
 *}
 
 (*<*)

--- a/Paper/document/root.bib	Wed Jun 30 16:56:37 2010 +0100
+++ b/Paper/document/root.bib	Thu Jul 01 01:53:00 2010 +0100
@@ -1,6 +1,7 @@
 @Inproceedings{Altenkirch10,
   author = {T.~Altenkirch and N.~A.~Danielsson and A.~L\"oh and N.~Oury},
   title =  {{PiSigma}: {D}ependent {T}ypes {W}ithout the {S}ugar},
+  booktitle = "Proc.~of the 10th FLOPS Conference",
   year = 2010,
   series = "LNCS",
   pages = "40--55",

--- a/Paper/document/root.tex	Wed Jun 30 16:56:37 2010 +0100
+++ b/Paper/document/root.tex	Thu Jul 01 01:53:00 2010 +0100
@@ -80,7 +80,7 @@
 convention already built in.
 \end{abstract}
 
-\category{CR-number}{subcategory}{third-level}
+%\category{F.4.1}{subcategory}{third-level}
 
 \terms
 formal reasoning, programming language calculi