# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1330534645 0
# Node ID 8fc6b801985bcd7ed3d6824a95e4fc8c60bfae25
# Parent  8be3155c014ff4ea7c134c307fecb64990a1d002
final changes to the lmcs paper

diff -r 8be3155c014f -r 8fc6b801985b LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Feb 29 16:23:11 2012 +0000
+++ b/LMCS-Paper/Paper.thy	Wed Feb 29 16:57:25 2012 +0000
@@ -2569,7 +2569,13 @@
   example the Core-Haskell language from the Introduction. With the work
   presented in this paper we can define it formally as shown in 
   Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
-  a corresponding reasoning infrastructure.
+  a corresponding reasoning infrastructure. However we have found out that 
+  telescopes seem to not easily representable in our framework. The reason is that
+  we need to be able to lift our @{text bn}-function to alpha-equated lambda-terms.
+  This requires restrictions, which class with the `global' scope of binders in
+  telescopes. They can
+  be represented in the framework desribed in \cite{WeirichYorgeySheard11} using an extension of
+  the usual locally-nameless representation. 
 
   \begin{figure}[p]
   \begin{boxedminipage}{\linewidth}
@@ -2679,16 +2685,27 @@
   definitions to equivariant functions (for them we can provide more
   automation).
 
-  There are some restrictions we imposed in this paper that we would like to lift in
-  future work. One is the exclusion of nested datatype definitions. Nested
+  There are some restrictions we imposed in this paper that can be lifted using 
+  a recent reimplementation \cite{Traytel12} of the datatype package for Isabelle/HOL, which
+  is however not yet part of the stable distribution.
+  This reimplementation allows nested
   datatype definitions would allow one to specify, for instance, the function kinds
   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
-  version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
-  achieve this, we need more clever implementation than we have 
-  at the moment. However, really lifting this restriction will involve major
-  work on the underlying datatype package of Isabelle/HOL.
+  version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). We can 
+  also use it to represent the @{text "Let"}-terms from the Introduction where
+  the order of @{text "let"}-assignments does not matter. This means we can represent @{text "Let"}s
+  such that the following two terms are equal
 
-  A more interesting line of investigation is whether we can go beyond the 
+  \[
+  @{text "Let x\<^isub>1 = t\<^isub>1 and x\<^isub>2 = t\<^isub>2 in s"} \;\;=\;\;
+  @{text "Let x\<^isub>2 = t\<^isub>2 and x\<^isub>1 = t\<^isub>1 in s"} 
+  \]\smallskip
+
+  \noindent
+  For this we have to represent the @{text "let"}-assignments as finite sets
+  of pair and a binding function that picks out the left components to be bound in @{text s}.
+
+  One line of investigation is whether we can go beyond the 
   simple-minded form of binding functions that we adopted from Ott. At the moment, binding
   functions can only return the empty set, a singleton atom set or unions
   of atom sets (similarly for lists). It remains to be seen whether 
@@ -2713,7 +2730,7 @@
   informal notes \cite{SewellBestiary} available to us and also for patiently
   explaining some of the finer points of the Ott-tool.  Stephanie Weirich
   suggested to separate the subgrammars of kinds and types in our Core-Haskell
-  example. Ramana Kumar and Andrei Popescu helped us with comments about 
+  example. Ramana Kumar and Andrei Popescu helped us with comments for
   an earlier version of this paper.
 *}
 
diff -r 8be3155c014f -r 8fc6b801985b LMCS-Paper/document/root.bib
--- a/LMCS-Paper/document/root.bib	Wed Feb 29 16:23:11 2012 +0000
+++ b/LMCS-Paper/document/root.bib	Wed Feb 29 16:57:25 2012 +0000
@@ -3,7 +3,7 @@
   author =       {D.~Traytel and A.~Popescu and J.~C.~Blanchette},
   title =        {{F}oundational, {C}ompositional ({C}o)datatypes for {H}igher-{O}rder 
                   {L}ogic: {C}ategory {T}heory {A}pplied to {T}heorem {P}roving},
-  note =         {Submitted for publication.},
+  note =         {Submitted for publication},
   year =         {2012}
 }
 
@@ -42,7 +42,8 @@
   author = 	 {S.~Weirich and B.~Yorgey and T.~Sheard},
   title = 	 {{B}inders {U}nbound},
   booktitle = 	 {Proc.~of the 16th International Conference on Functional Programming (ICFP)},
-  year = 	 {2011}
+  year = 	 {2011},
+  pages =        {333-345}
 }
 
 @InProceedings{UrbanKaliszyk11,