# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276169318 -7200
# Node ID 502eaa199726e74ea599cb7233cc0c0b365ade48
# Parent  fc5bfd0cc1cda117bde99798b8418cee3e35c05c
added to the popl-paper a pointer to work by Altenkirch

diff -r fc5bfd0cc1cd -r 502eaa199726 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Jun 10 10:53:51 2010 +0200
+++ b/Paper/Paper.thy	Thu Jun 10 13:28:38 2010 +0200
@@ -115,7 +115,9 @@
   that can be used to faithfully represent this kind of binding in Nominal
   Isabelle.  The difficulty of finding the right notion for alpha-equivalence
   can be appreciated in this case by considering that the definition given by
-  Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
+  Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). A related
+  notion of alpha-equivalence that allows vacuous binders, there called weakening 
+  of contexts, is defined in for the $\Pi\Sigma$-calculus \cite{Altenkirch10}.
 
   However, the notion of alpha-equivalence that is preserved by vacuous
   binders is not always wanted. For example in terms like
@@ -154,7 +156,7 @@
   \begin{center}
   @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
   \end{center}
-
+  %
   \noindent
   As a result, we provide three general binding mechanisms each of which binds
   multiple variables at once, and let the user chose which one is intended
@@ -364,9 +366,8 @@
   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
   proofs, we establish a reasoning infrastructure for alpha-equated
   terms, including properties about support, freshness and equality
-  conditions for alpha-equated terms. We are also able to derive, for the moment 
-  only manually, strong induction principles that 
-  have the variable convention already built in.
+  conditions for alpha-equated terms. We are also able to derive strong 
+  induction principles that have the variable convention already built in.
 
   \begin{figure}
   \begin{boxedminipage}{\linewidth}
@@ -2017,11 +2018,20 @@
   inter-translated, but we have not proved this. However, we believe the
   binding specifications in the style of Ott are a more natural way for 
   representing terms involving bindings. Pottier gives a definition for 
-  alpha-equivalence, which is similar to our binding mod \isacommand{bind}. 
+  alpha-equivalence, which is similar to our binding mode \isacommand{bind}. 
   Although he uses also a permutation in case of abstractions, his
   definition is rather different from ours. He proves that his notion
   of alpha-equivalence is indeed a equivalence relation, but a complete
   reasoning infrastructure is well beyond the purposes of his language. 
+  In a slightly different domain (programming with dependent types), the 
+  paper \cite{Altenkirch10} presents a calculus with a notion of 
+  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
+  equality between terms also includes rules for $\beta$ and to our
+  knowledge no concrete mathematical result concerning their notion
+  of equality has been proved.    
 *}
 
 section {* Conclusion *}
diff -r fc5bfd0cc1cd -r 502eaa199726 Paper/document/root.bib
--- a/Paper/document/root.bib	Thu Jun 10 10:53:51 2010 +0200
+++ b/Paper/document/root.bib	Thu Jun 10 13:28:38 2010 +0200
@@ -1,3 +1,13 @@
+@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},
+  year = 2010,
+  series = "LNCS",
+  pages = "40--55",
+  volume = 6009
+}
+
+
 @InProceedings{ UrbanTasson05,
 	author = "C. Urban and C. Tasson",
 	title = "{N}ominal {T}echniques in {I}sabelle/{HOL}",