# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269997158 -7200
# Node ID 2eafd8ed4bbf5ca0287718bacc0622601fba442c
# Parent  1801cc460fc92734ac50a7b6b24cae7d09d48fd2
started with a related work section

diff -r 1801cc460fc9 -r 2eafd8ed4bbf Paper/Paper.thy
--- 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
+    
 
   
 *}
diff -r 1801cc460fc9 -r 2eafd8ed4bbf Paper/document/root.bib
--- a/Paper/document/root.bib	Tue Mar 30 22:31:15 2010 +0200
+++ b/Paper/document/root.bib	Wed Mar 31 02:59:18 2010 +0200
@@ -1,3 +1,27 @@
+@InProceedings{LeeCraryHarper07,
+  author = 	 {D.~K.~Lee and K.~Crary and R.~Harper},
+  title = 	 {{T}owards a {M}echanized {M}etatheory of {Standard ML}},
+  booktitle =    {Proc.~of the 34th POPL Symposium},
+  year = 	 2007,
+  pages =        {173--184}
+}
+
+@Unpublished{chargueraud09,
+  author       = "Arthur Chargu{\'e}raud",
+  title        = "{T}he {L}ocally {N}ameless {R}epresentation",
+  year         = "2009",
+  note         = "To appear in J.~of Automated Reasoning. 
+                  {http://arthur.chargueraud.org/research/2009/ln/}",
+}
+
+@article{NaraschewskiNipkow99,
+  author={W.~Naraschewski and T.~Nipkow},
+  title={{T}ype {I}nference {V}erified: {A}lgorithm {W} in {Isabelle/HOL}},
+  journal={J.~of Automated Reasoning},
+  year=1999,
+  volume=23,
+  pages={299--318}}
+
 @InProceedings{Berghofer99,
   author = 	 {S.~Berghofer and M.~Wenzel},
   title = 	 {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in 
@@ -142,8 +166,8 @@
 
 @article{Pitts03,
   author =	 {A.~M.~Pitts},
-  title =	 {Nominal Logic, A First Order Theory of Names and
-                  Binding},
+  title =	 {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and
+                  {B}inding},
   journal =	 {Information and Computation},
   year =	 {2003},
   volume =	 {183},