--- a/Paper/Paper.thy	Thu Mar 18 19:39:01 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 22:06:28 2010 +0100
@@ -15,16 +15,16 @@
 section {* Introduction *}
 
 text {*
-  So far, Nominal Isabelle provided a mechanism to construct
-  automatically alpha-equated lambda terms sich as
+  So far, Nominal Isabelle provides a mechanism for constructing
+  automatically alpha-equated terms such as
 
   \begin{center}
   $t ::= x \mid t\;t \mid \lambda x. t$
   \end{center}
 
   \noindent
-  For such calculi, it derived automatically a convenient reasoning
-  infrastructure. With this it has been used to formalise an equivalence
+  For such terms it derives automatically a reasoning
+  infrastructure, which has been used in formalisations of an equivalence
   checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
   \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result
@@ -32,9 +32,9 @@
   used by Pollack for formalisations in the locally-nameless approach to
   binding \cite{SatoPollack10}.
 
-  However, Nominal Isabelle has fared less well in a formalisation of
-  the algorithm W \cite{UrbanNipkow09} where types and type-schemes
-  are represented by
+  However, Nominal Isabelle fared less well in a formalisation of
+  the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
+  are of the form
 
   \begin{center}
   \begin{tabular}{l}
@@ -43,108 +43,115 @@
   \end{center}
 
   \noindent
-  While it is possible to formalise the finite set of variables that are
-  abstracted in a type-scheme by iterating single abstractions, it leads to a very
-  clumsy formalisation. This need of iterating single binders for representing
-  multiple binders is also the reason why Nominal Isabelle and other theorem
-  provers have so far not fared very well with the more advanced tasks in the POPLmark
-  challenge, because also there one would like to abstract several variables 
+  and the quantification abstracts over a finite (possibly empty) set of type variables.
+  While it is possible to formalise such abstractions by iterating single bindings, 
+  it leads to a very clumsy formalisation of W. This need of iterating single binders 
+  for representing multiple binders is also the reason why Nominal Isabelle and other 
+  theorem provers have not fared extremely well with the more advanced tasks 
+  in the POPLmark challenge \cite{challenge05}, because also there one would be able 
+  to aviod clumsy reasoning if there were a mechanisms for abstracting several variables 
   at once.
 
-  There are interesting points to note with binders that abstract multiple 
-  variables. First in the case of type-schemes we do not like to make a distinction
-  about the order of the binders. So we would like to regard the following two
-  type-schemes as alpha-equivalent:
+  To see this, let us point out some interesting properties of binders abstracting multiple 
+  variables. First, in the case of type-schemes, we do not like to make a distinction
+  about the order of the bound variables. Therefore we would like to regard the following two
+  type-schemes as alpha-equivalent
 
   \begin{center}
   $\forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ 
   \end{center}
 
   \noindent
-  but assuming $x$, $y$ and $z$ are distinct, the following two should be \emph{not} 
-  alpha-equivalent:
+  but  the following two should \emph{not} be alpha-equivalent
 
   \begin{center}
   $\forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ 
   \end{center}
 
   \noindent
-  However we do like to regard type-schemes as alpha-equivalent, if they
-  differ only on \emph{vacuous} binders, such as
+  assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as 
+  alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
 
   \begin{center}
   $\forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ 
   \end{center}
 
   \noindent
-  In this paper we will give a general abstraction mechanism and assciated notion of alpha-equivalence 
-  which can be used to represent type-schemes.  The difficulty in finding the notion of alpha-equivalence 
-  can be appreciated by considering that the definition given by Leroy in \cite{Leroy92} is incorrect 
-  (it omits a side-condition).
+  In this paper we will give a general abstraction mechanism and associated
+  notion of alpha-equivalence that can be used to faithfully represent
+  type-schemes in Nominal Isabelle.  The difficulty of finding the right notion 
+  for alpha-equivalence in this case can be appreciated by considering that the 
+  definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
+
+
 
   However, the notion of alpha-equivalence that is preserved by vacuous binders is not
-  alway wanted. For example in constructs like
+  alway wanted. For example in terms like
 
   \begin{center}
-  $\LET x = 3 \AND y = 2 \IN x \backslash y \END$
+  $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$
   \end{center}
 
   \noindent
-  we might not care in which order the associations $x = 3$ and $y = 2$ are
-  given, but it would be unusual to regard this term as alpha-equivalent with
+  we might not care in which order the assignments $x = 3$ and $y = 2$ are
+  given, but it would be unusual to regard the above term as alpha-equivalent 
+  with
 
   \begin{center}
-  $\LET x = 3 \AND y = 2 \AND z = loop \IN x \backslash y \END$
+  $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,\backslash\,y \END$
   \end{center}
 
   \noindent
-  We will provide a separate abstraction mechanism for this case where the
-  order of binders does not matter, but the ``cardinality'' of the binders
-  has to be the same.
+  Therefore we will also provide a separate abstraction mechanism for cases 
+  in which the order of binders does not matter, but the ``cardinality'' of the 
+  binders has to be the same.
 
-  However, this is still not sufficient for covering language constructs frequently 
-  occuring in programming language research. For example in patters like
+  However, we found that this is still not sufficient for covering language 
+  constructs frequently occuring in programming language research. For example 
+  in $\mathtt{let}$s involving patterns 
 
   \begin{center}
-  $\LET (x, y) = (3, 2) \IN x \backslash y \END$
+  $\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$
   \end{center}
 
   \noindent
   we want to bind all variables from the pattern (there might be an arbitrary
-  number of them) inside the body of the let, but we also care about the order
-  of these variables, since we do not want to identify this term with
+  number of them) inside the body of the $\mathtt{let}$, but we also care about 
+  the order of these variables, since we do not want to identify the above term 
+  with
 
   \begin{center}
-  $\LET (y, x) = (3, 2) \IN x \backslash y \END$
+  $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$
   \end{center}
 
   \noindent
-  Therefore we have identified three abstraction mechanisms for multiple binders
-  and allow the user to chose which one is intended. 
+  As a result, we provide three general abstraction mechanisms for multiple binders
+  and allow the user to chose which one is intended when formalising a
+  programming language calculus.
 
-  By providing general abstraction mechanisms that allow the binding of multiple
-  variables, we have to work around aproblem that has been first pointed out
-  by Pottier in \cite{Pottier}: in let-constructs such as
+  By providing these general abstraction mechanisms, however, we have to work around 
+  a problem that has been pointed out by Pottier in \cite{Pottier06}: in 
+  $\mathtt{let}$-constructs of the form
 
   \begin{center}
   $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
   \end{center}
 
   \noindent
-  where the $x_i$ are bound in $s$. In this term we might not care about the order in 
+  which bind all the $x_i$ in $s$, we might not care about the order in 
   which the $x_i = t_i$ are given, but we do care about the information that there are 
-  as many $x_i$ as there are $t_i$. We lose this information if we specify the 
+  as many $x_i$ as there are $t_i$. We lose this information if we represent the 
   $\mathtt{let}$-constructor as something like 
 
   \begin{center}
-  $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$
+  $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
   \end{center}
 
   \noindent
-  where the $[\_].\_$ indicates that a list of variables become bound
+  where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes bound
   in $s$. In this representation we need additional predicates to ensure 
   that the two lists are of equal length. This can result into very 
-  elaborate reasoning (see \cite{BengtsonParow09}). 
+  unintelligible reasoning (see for example~\cite{BengtsonParow09}). 
   
   
 

--- a/Paper/document/root.bib	Thu Mar 18 19:39:01 2010 +0100
+++ b/Paper/document/root.bib	Thu Mar 18 22:06:28 2010 +0100
@@ -9,6 +9,16 @@
   series = 	 {LNCS}
 }
 
+@INPROCEEDINGS{Pottier06,
+  author = {F.~Pottier},
+  title = {{A}n {O}verview of {C$\alpha$ml}},
+  year = {2006},
+  booktitle = {ACM Workshop on ML},
+  pages = {27--52},
+  volume = {148},
+  number = {2},
+  series = {ENTCS}
+}
 
 @Unpublished{HuffmanUrban10,
   author = 	 {B.~Huffman and C.~Urban},
@@ -32,6 +42,21 @@
   note = 	 {Personal communication.}
 }
 
+@InProceedings{challenge05,
+  author = 	 {B.~E.~Aydemir and A.~Bohannon and M.~Fairbairn and
+                  J.~N.~Foster and B.~C.~Pierce and P.~Sewell and 
+                  D.~Vytiniotis and G.~Washburn and S.~Weirich and
+                  S.~Zdancewic},
+  title = 	 {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark 
+                  {C}hallenge},
+  booktitle = 	 {Proc.~of the 18th International Conference on Theorem Proving in Higher-Order 
+                  Logics (TPHOLs)},
+  pages = 	 {50--65},
+  year = 	 {2005},
+  volume = 	 {3603},
+  series = 	 {LNCS}
+}
+
 @Unpublished{SatoPollack10,
   author = 	 {M.~Sato and R.~Pollack},
   title = 	 {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},

--- a/Paper/document/root.tex	Thu Mar 18 19:39:01 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 22:06:28 2010 +0100
@@ -48,13 +48,13 @@
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about
 programming language calculi. In this paper we present an extension of Nominal
-Isabelle for dealing with general binding structures. Such binding structures
+Isabelle in order to deal with general binding structures. Such binding structures
 are ubiquitous in programming language research and only very poorly supported
-by theorem provers providing only single binding as in the lambda-calculus. We
-give in this paper novel definitions for alpha-equivalence and establish
-automatically the reasoning structure for alpha-equated terms. For example we
-provide a strong induction principle that has the variable convention already
-built in.
+with single binders, as for example found in the lambda-calculus. For our
+extension we introduce novel definitions of alpha-equivalence and establish
+automatically the reasoning infrastructure for alpha-equated terms. This
+includes a strong induction principle which has the variable convention
+already built in.
 \end{abstract}