--- a/Paper/Paper.thy	Tue Mar 30 22:31:15 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 02:59:18 2010 +0200
@@ -1530,9 +1530,35 @@
 section {* Related Work *}
 
 text {*
-  Ott is better with list dot specifications; subgrammars
+  The earliest usage we know of general binders in a theorem prover setting is 
+  in the paper \cite{NaraschewskiNipkow99}, which describes a formalisation of 
+  the algorithm W. This formalisation implements binding in type schemes using a 
+  a de-Bruijn indices representation. Also recently an extension for general binders 
+  has been proposed for the locally nameless approach to binding \cite{chargueraud09}. .
+  But we have not yet seen it to be employed in a non-trivial formal verification.
+  In both approaches, it seems difficult to achieve our fine-grained control over the
+  ``semantics'' of bindings (whether the order should matter, or vacous binders 
+  should be taken into account). To do so, it is necessary to introduce predicates 
+  that filter out some unwanted terms. This very likely results in intricate 
+  formal reasoning.
+ 
+  Higher-Order Abstract Syntax (HOAS) approaches to representing binders are
+  nicely supported in the Twelf theorem prover and work is in progress to use
+  HOAS in a mechanisation of the metatheory of SML
+  \cite{LeeCraryHarper07}. HOAS supports elegantly reasoning about
+  term-calculi with single binders. We are not aware how more complicated
+  binders from SML are represented in HOAS, but we know that HOAS cannot
+  easily deal with binding constructs where the number of bound variables is
+  not fixed. An example is the second part of the POPLmark challenge where
+  @{text "Let"}s involving patterns need to be formalised. In such situations
+  HOAS needs to use essentially has to represent multiple binders with
+  iterated single binders.
 
-  untyped; 
+  An attempt of representing general binders in the old version of Isabelle 
+  based also on iterating single binders is described in \cite{BengtsonParow09}. 
+  The reasoning there turned out to be quite complex. 
+
+  Ott is better with list dot specifications; subgrammars, is untyped; 
   
 *}
 
@@ -1543,6 +1569,10 @@
   Complication when the single scopedness restriction is lifted (two 
   overlapping permutations)
 
+  Future work: distinct list abstraction
+
+  TODO: function definitions:
+  
 
   The formalisation presented here will eventually become part of the 
   Isabelle distribution, but for the moment it can be downloaded from 
@@ -1552,10 +1582,6 @@
 *}
 
 text {*
-
-  TODO: function definitions:
-  \medskip
-
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
   many discussions about Nominal Isabelle. We thank Peter Sewell for 
@@ -1565,9 +1591,7 @@
   also thank Stephanie Weirich for suggesting to separate the subgrammars
   of kinds and types in our Core-Haskell example.
 
-  Lookup: Merlin paper by James Cheney; Mark Shinwell PhD
-
-  Future work: distinct list abstraction
+    
 
   
 *}