- new naming sheme for documentation yields more stable names

- update for document J2a

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 40ff9c8b5d2a7c03bf380c2d017c5eac8dec55be..b84be907c731d3a5fd0896005feacfb9a445da0d 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -222,6 +222,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:39 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index e6ecc8d7c3dc55fb70d714c1510e9bca454b8a3c..f169633b0d418c5cfd80bcba37ab2b9441dc3df7 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -258,6 +258,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index 739454623d63d475385335801e071c8b01ee6639..87daf7e4141095d1860aea13ec292671e72bccad 100644 (file)
--- a/helm/www/lambdadelta/basic_1.html
+++ b/helm/www/lambdadelta/basic_1.html
@@ -102,7 +102,7 @@
         </tbody>
       </table>
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="blocks">Abstract Syntax and Behavior <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="">Abstract Syntax and Behavior <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">This is a summary of available syntactic items and reductions (block structure).
    </div>
@@ -823,6 +823,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 05 Mar 2015 16:42:28 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 76d0594a8782e072eb5905e28d245465f1599290..d41e116cf2eac65bae2879d4cc92664f7a3dec76 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -1384,6 +1384,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 5f7506bd5b8bb7beaf00f0f2a23d2447cceaadd5..2b367888d859482710e21085a7a6e2e9c54ed844 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -110,21 +110,21 @@
       <a href="http://lambdadelta.info/download/lambdadelta.bib">lambdadelta.bib</a>,
       <span class="emph alpha">view</span>
       <a href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
-      (revised <span class="emph gamma">2014-10</span>).
+      (revised <span class="emph gamma">2015-03</span>).
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v3">
       <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b8.png" /> λδ version 3 (proposed)</div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      The main source of information is <span class="emph alpha">J4</span>.
+      The main source of information is <span class="emph alpha">J3a</span>.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>
-            <td class="snns top" id="ldJ4">
-              <span class="emph alpha">J4.</span>
+            <td class="snns top" id="ldJ3a">
+              <span class="emph alpha">J3a.</span>
             </td>
-            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/gda.pdf">A Verified Translation of Landau's "Grundlagen" from Automath into a Pure Type System, via λδ</a> (<span class="emph alpha">2015-02</span>). Submitted to JFR, Univerity of Bologna.</td>
+            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/gda.pdf">A Verified Translation of Landau's "Grundlagen" from Automath into a Pure Type System, via λδ</a> (<span class="emph alpha">2015-02</span>). Submitted to JFR, Univerity of Bologna. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
           <tr>
             <td class="nnss top" />
@@ -138,16 +138,16 @@
     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
       <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      The main source of information is <span class="emph alpha">J2</span>.
+      The main source of information is <span class="emph alpha">J2a</span>.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>
-            <td class="snns top" id="ldJ2">
-              <span class="emph alpha">J2.</span>
+            <td class="snns top" id="ldJ2a">
+              <span class="emph alpha">J2a.</span>
             </td>
-            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/basic2a.pdf">The Formal System λδ Revised - Stage A: Extending the Applicability Condition</a> (<span class="emph gamma">2014-11</span>). Submitted to ACM ToCL. CoRR identifier <a href="http://arxiv.org/abs/1411.0154">1411.0154</a> [v1].</td>
+            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/basic2a.pdf">The Formal System λδ Revised, Stage A: Extending the Applicability Condition</a> (<span class="emph gamma">2014-11</span>). Submitted to ACM ToCL. CoRR identifier <a href="http://arxiv.org/abs/1411.0154">1411.0154</a> [v2] (revised <span class="emph gamma">2015-03</span>). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
           <tr>
             <td class="nnns top" />
@@ -156,8 +156,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldR5">
-              <span class="emph alpha">R5.</span>
+            <td class="snns top" id="ldR2b">
+              <span class="emph alpha">R2b.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/cie_2010.pdf">An Efficient Validation Procedure for the Formal System λδ</a> (<span class="emph alpha">2010-07</span>). In CiE 2010 Local Proceedings. University of Azores, CMATI Booklet, pp. 204-213. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
@@ -168,8 +168,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldR4">
-              <span class="emph alpha">R4.</span>
+            <td class="snns top" id="ldR2a">
+              <span class="emph alpha">R2a.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16">Landau's "Grundlagen der Analysis" from Automath to lambda-delta</a> (<span class="emph alpha">2009-09</span>). University of Bologna, technical report UBLCS-2009-16. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
@@ -180,8 +180,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldP8">
-              <span class="emph alpha">P8.</span>
+            <td class="snns top" id="ldP2c">
+              <span class="emph alpha">P2c.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_8s.pdf">The Formal System λδ and the "Three Problems"</a> (<span class="emph beta">2014-06</span>). Presentation at University of Bologna (slides).</td>
           </tr>
@@ -192,8 +192,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldP7">
-              <span class="emph alpha">P7.</span>
+            <td class="snns top" id="ldP2b">
+              <span class="emph alpha">P2b.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_7s.pdf">An Efficient Validation Procedure for the Formal System λδ</a> (<span class="emph alpha">2010-07</span>). Presentation at CiE 2010 (slides).</td>
           </tr>
@@ -204,8 +204,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldP6">
-              <span class="emph alpha">P6.</span>
+            <td class="snns top" id="ldP2a">
+              <span class="emph alpha">P2a.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_6s.pdf">A Validator for the Formal System λδ</a> (revised <span class="emph alpha">2010-02</span>). Presentation at University of Bologna (slides).</td>
           </tr>
@@ -234,7 +234,7 @@
       <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (superseded)</div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       The main source of information is <span class="emph alpha">J1</span>.
-      A summary is available in <span class="emph alpha">P5</span>.
+      A summary is available in <span class="emph alpha">P1e</span>.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       <table cellpadding="4" cellspacing="0">
@@ -253,8 +253,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldR3">
-              <span class="emph alpha">R3.</span>
+            <td class="snns top" id="ldR1c">
+              <span class="emph alpha">R1c.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/cie_2007.pdf">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="emph delta">2007-06</span>). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
@@ -265,8 +265,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldR2">
-              <span class="emph alpha">R2.</span>
+            <td class="snns top" id="ldR1b">
+              <span class="emph alpha">R1b.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="emph gamma">2006-11</span>). University of Bologna, technical report UBLCS-2006-25. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
@@ -277,8 +277,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldR1">
-              <span class="emph alpha">R1.</span>
+            <td class="snns top" id="ldR1a">
+              <span class="emph alpha">R1a.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01">Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification</a> (<span class="emph beta">2006-01</span>). University of Bologna, technical report UBLCS-2006-01. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
@@ -289,8 +289,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldP5">
-              <span class="emph alpha">P5.</span>
+            <td class="snns top" id="ldP1e">
+              <span class="emph alpha">P1e.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_5s.pdf">The Formal System λδ</a> (<span class="emph delta">2008-10</span>). Presentation at Advances in Constructive Topology and Logical Foundations (slides).</td>
           </tr>
@@ -301,8 +301,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldP4">
-              <span class="emph alpha">P4.</span>
+            <td class="snns top" id="ldP1d">
+              <span class="emph alpha">P1d.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_4s.pdf">Towards the Unification of Terms, Types and Contexts</a> (<span class="emph gamma">2008-03</span>). Presentation at Types 2008 (slides).</td>
           </tr>
@@ -313,8 +313,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldP3">
-              <span class="emph alpha">P3.</span>
+            <td class="snns top" id="ldP1c">
+              <span class="emph alpha">P1c.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_3s.pdf">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="emph gamma">2007-06</span>). Presentation at CiE 2007 (slides).</td>
           </tr>
@@ -325,8 +325,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldP2">
-              <span class="emph alpha">P2.</span>
+            <td class="snns top" id="ldP1b">
+              <span class="emph alpha">P1b.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_2s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni</a> (<span class="emph gamma">2007-01</span>). Presentation at University of Padova (slides <span class="emph alpha">in Italian</span>).</td>
           </tr>
@@ -337,8 +337,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldP1">
-              <span class="emph alpha">P1.</span>
+            <td class="snns top" id="ldP1a">
+              <span class="emph alpha">P1a.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_1s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata</a> (<span class="emph beta">2005-12</span>). Presentation at University of Bologna (slides <span class="emph alpha">in Italian</span>).</td>
           </tr>
@@ -352,7 +352,7 @@
             <td class="snns top" id="ldV1">
               <span class="emph alpha">V1.</span>
             </td>
-            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_1.html">lambdadelta_1</a> (revised <span class="emph delta">2012-10</span>). Formal specification for the proof assistant Coq 7.3.1 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_1.html">lambdadelta_1</a> (revised <span class="emph delta">2015-01</span>). Formal specification for the proof assistant Coq 7.3.1 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
           <tr>
             <td class="nnss top" />
@@ -389,6 +389,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/download/basic2a.pdf b/helm/www/lambdadelta/download/basic2a.pdf
index 74cbdc164e7465d3efb32c9aae0a5c3217202983..e47b376d90969f21ca3595373f7a34e393032243 100644 (file)
Binary files a/helm/www/lambdadelta/download/basic2a.pdf and b/helm/www/lambdadelta/download/basic2a.pdf differ

diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib
index dce057e235d9389b329624bcc6afeb4b3bd90db7..080080f381f18c4072476a3ffd7047e9608dd7f7 100644 (file)
--- a/helm/www/lambdadelta/download/lambdadelta.bib
+++ b/helm/www/lambdadelta/download/lambdadelta.bib
@@ -1,6 +1,6 @@
 % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadeltaJ4,
+@misc{lambdadeltaJ3a,
    author="F. {Guidi}",
    title="{A Verified Translation of Landau's `Grundlagen'' from Automath into a Pure Type System, via $\lambda\delta$}",
    year="2015",
@@ -10,9 +10,9 @@
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadeltaJ2,
+@misc{lambdadeltaJ2a,
    author="F. {Guidi}",
-   title="{The Formal System $\lambda\delta$ Revised - Stage A: Extending the Applicability Condition}",
+   title="{The Formal System $\lambda\delta$ Revised, Stage A: Extending the Applicability Condition}",
    howpublished="CoRR identifier 1411.0154",
    year="2014",
    month="November",
@@ -28,7 +28,7 @@
    note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$"
 }
 
-@incollection{lambdadeltaR5,
+@incollection{lambdadeltaR2b,
    author="F. {Guidi}", 
    title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
    editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
@@ -40,7 +40,7 @@
    month="July"
 }
 
-@techreport{lambdadeltaR4,
+@techreport{lambdadeltaR2a,
    author="F. {Guidi}", 
    title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", 
    type="Technical Report",
@@ -66,7 +66,7 @@
    month="November"
 }
 
-@incollection{lambdadeltaR3,
+@incollection{lambdadeltaR1c,
    author="F. {Guidi}", 
    title="{Lambda Types on the Lambda Calculus with Abbreviations}",
    editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
@@ -78,7 +78,7 @@
    month="June"
 }
 
-@techreport{lambdadeltaR2,
+@techreport{lambdadeltaR1b,
    author="F. {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", 
    type="Technical Report",
@@ -89,7 +89,7 @@
    month="November"
 }
 
-@techreport{lambdadeltaR1,
+@techreport{lambdadeltaR1a,
    author="F. {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", 
    type="Technical Report",

diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt
index dce057e235d9389b329624bcc6afeb4b3bd90db7..080080f381f18c4072476a3ffd7047e9608dd7f7 100644 (file)
--- a/helm/www/lambdadelta/download/lambdadelta.txt
+++ b/helm/www/lambdadelta/download/lambdadelta.txt
@@ -1,6 +1,6 @@
 % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadeltaJ4,
+@misc{lambdadeltaJ3a,
    author="F. {Guidi}",
    title="{A Verified Translation of Landau's `Grundlagen'' from Automath into a Pure Type System, via $\lambda\delta$}",
    year="2015",
@@ -10,9 +10,9 @@
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadeltaJ2,
+@misc{lambdadeltaJ2a,
    author="F. {Guidi}",
-   title="{The Formal System $\lambda\delta$ Revised - Stage A: Extending the Applicability Condition}",
+   title="{The Formal System $\lambda\delta$ Revised, Stage A: Extending the Applicability Condition}",
    howpublished="CoRR identifier 1411.0154",
    year="2014",
    month="November",
@@ -28,7 +28,7 @@
    note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$"
 }
 
-@incollection{lambdadeltaR5,
+@incollection{lambdadeltaR2b,
    author="F. {Guidi}", 
    title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
    editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
@@ -40,7 +40,7 @@
    month="July"
 }
 
-@techreport{lambdadeltaR4,
+@techreport{lambdadeltaR2a,
    author="F. {Guidi}", 
    title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", 
    type="Technical Report",
@@ -66,7 +66,7 @@
    month="November"
 }
 
-@incollection{lambdadeltaR3,
+@incollection{lambdadeltaR1c,
    author="F. {Guidi}", 
    title="{Lambda Types on the Lambda Calculus with Abbreviations}",
    editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
@@ -78,7 +78,7 @@
    month="June"
 }
 
-@techreport{lambdadeltaR2,
+@techreport{lambdadeltaR1b,
    author="F. {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", 
    type="Technical Report",
@@ -89,7 +89,7 @@
    month="November"
 }
 
-@techreport{lambdadeltaR1,
+@techreport{lambdadeltaR1a,
    author="F. {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", 
    type="Technical Report",

diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
index f8e72014b71be7e4cbdeecf496331facc97ad5d9..a9f2cf2bf1001c1774f86a4e1822f026a20c62a7 100644 (file)
--- a/helm/www/lambdadelta/ground_1.html
+++ b/helm/www/lambdadelta/ground_1.html
@@ -275,6 +275,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index b2cc62e277b9eb90b8e5a70c1760f96d2b29971f..a8f176a5a46b3941c8698dd6fad7d83db50dfabc 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -328,6 +328,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index f0e1d32ffe2616bfbb3397061e2a04bae253f26f..6e429e20df3b216f90a70475d67ad7e3d925544e 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -157,7 +157,7 @@
       (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
       The overall validation speed of the "Grundlagen der Analysis"
       increases of 34% with respect to version 0.8.1.
-      <a href="http://lambdadelta.info/documentation.html#ldJ4">Documentation (J4)</a>.
+      <a href="http://lambdadelta.info/documentation.html#ldJ3a">Documentation (J3a)</a>.
       [Svn revision: 13035] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>).
       <ul>
           <li>
@@ -220,7 +220,7 @@
       Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
       and exportation to <a href="http://www.w3.org/XML/">XML</a>.
-      <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.
+      <a href="http://lambdadelta.info/documentation.html#ldR2a">Documentation (R2a)</a>.
       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
       <ul>
           <li>
@@ -269,6 +269,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 317de931de474ab0f75b518235824c941c253c97..047fffc785b56d0480a3f26abab5e58e12ff6eea 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -202,6 +202,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 3b45a688cdfd82b3555acbf7c9e66616a59cf567..267710b06076a99945140080cf3d2dbdd8264d30 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -146,7 +146,7 @@
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph gamma">October 2014.</span>
-        <a href="http://lambdadelta.info/documentation.html#ldJ2">λδ version 2A</a>
+        <a href="http://lambdadelta.info/documentation.html#ldJ2a">λδ version 2A</a>
       is released.
    </li>
     </ul>
@@ -159,7 +159,7 @@
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph beta">June 2014.</span>
-        <a href="http://lambdadelta.info/documentation.html#ldP8">First communication on λδ version 2.</a>
+        <a href="http://lambdadelta.info/documentation.html#ldP2c">First communication on λδ version 2.</a>
       </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
@@ -292,14 +292,14 @@
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph gamma">November 2006.</span>
-        <a href="http://lambdadelta.info/documentation.html#ldR2">λδ version 1</a>
+        <a href="http://lambdadelta.info/documentation.html#ldR1b">λδ version 1</a>
       is released.
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph beta">December 2005.</span>
-        <a href="http://lambdadelta.info/documentation.html#ldP1">First communication on λδ version 1</a>.
+        <a href="http://lambdadelta.info/documentation.html#ldP1a">First communication on λδ version 1</a>.
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
@@ -354,6 +354,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 05 Mar 2015 16:46:30 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index e4fab58998ae5f49c0e5b2a706164bc7f4d0fc19..08d1f256edcc17a52d3bc92cd507fa453cbaaabf 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -328,6 +328,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 06 Mar 2015 16:17:54 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml
index a51f64307e740bf753974dde89a84b41d80f7cd8..bfcf845270b12a8c2b3aebabac2d0280b3cd7585 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml
@@ -14,25 +14,25 @@
       <rlink to="download/lambdadelta.bib">lambdadelta.bib</rlink>,
       <notice class="alpha" notice="view"/>
       <rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
-      (revised <notice class="gamma" notice="2014-10"/>).
+      (revised <notice class="gamma" notice="2015-03"/>).
    </body>
 
    <subsection name="v3"><version3-icon/>λδ version 3 (proposed)</subsection>
    <body>
-      The main source of information is <notice class="alpha" notice="J4"/>.
+      The main source of information is <notice class="alpha" notice="J3a"/>.
    </body>
    <table name="documentation_3"/>
    
    <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
    <body>
-      The main source of information is <notice class="alpha" notice="J2"/>.
+      The main source of information is <notice class="alpha" notice="J2a"/>.
    </body>
    <table name="documentation_2"/>
 
    <subsection name="v1"><version1-icon/>λδ version 1 (superseded)</subsection>
    <body>
       The main source of information is <notice class="alpha" notice="J1"/>.
-      A summary is available in <notice class="alpha" notice="P5"/>.
+      A summary is available in <notice class="alpha" notice="P1e"/>.
    </body>
    <table name="documentation_1"/>
 

diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl
index a12c186836c5a8a8eb640a47b450d44c9db924b6..65ba896680fb8ccea07352cbd1947f075859788c 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_1.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_1.tbl
@@ -16,7 +16,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldR3" "<span class=\"emph alpha\">R3.</span>" "" } {
+   [ { name "ldR1c" "<span class=\"emph alpha\">R1c.</span>" "" } {
      "F. Guidi:" +
      @@("download/cie_2007.pdf"
      "Lambda Types on the Lambda Calculus with Abbreviations") +
@@ -27,7 +27,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldR2" "<span class=\"emph alpha\">R2.</span>" "" } {
+   [ { name "ldR1b" "<span class=\"emph alpha\">R1b.</span>" "" } {
      "F. Guidi:" +
      @("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25"
      "Lambda Types on the Lambda Calculus with Abbreviations") +
@@ -36,7 +36,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldR1" "<span class=\"emph alpha\">R1.</span>" "" } {
+   [ { name "ldR1a" "<span class=\"emph alpha\">R1a.</span>" "" } {
      "F. Guidi:" +
      @("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01"
      "Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification") +
@@ -45,14 +45,14 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldP5" "<span class=\"emph alpha\">P5.</span>" "" } {
+   [ { name "ldP1e" "<span class=\"emph alpha\">P1e.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_5s.pdf" "The Formal System λδ") +
      "(<span class=\"emph delta\">2008-10</span>)." +
      "Presentation at Advances in Constructive Topology and Logical Foundations (slides)."
      * }
    ]
-   [ { name "ldP4" "<span class=\"emph alpha\">P4.</span>" "" } {
+   [ { name "ldP1d" "<span class=\"emph alpha\">P1d.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_4s.pdf"
      "Towards the Unification of Terms, Types and Contexts") +
@@ -60,7 +60,7 @@ table {
      "Presentation at Types 2008 (slides)."
      * }
    ]
-   [ { name "ldP3" "<span class=\"emph alpha\">P3.</span>" "" } {
+   [ { name "ldP1c" "<span class=\"emph alpha\">P1c.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_3s.pdf"
      "Lambda Types on the Lambda Calculus with Abbreviations") +
@@ -68,7 +68,7 @@ table {
      "Presentation at CiE 2007 (slides)."
      * }
    ]
-   [ { name "ldP2" "<span class=\"emph alpha\">P2.</span>" "" } {
+   [ { name "ldP1b" "<span class=\"emph alpha\">P1b.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_2s.pdf"
      "Lambda Tipi sul Lambda Calcolo con Abbreviazioni") +
@@ -77,7 +77,7 @@ table {
      "<span class=\"emph alpha\">in Italian</span>)."
      * }
    ]
-   [ { name "ldP1" "<span class=\"emph alpha\">P1.</span>" "" } {
+   [ { name "ldP1a" "<span class=\"emph alpha\">P1a.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_1s.pdf"
      "Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata") +
@@ -89,7 +89,7 @@ table {
    [ { name "ldV1" "<span class=\"emph alpha\">V1.</span>" "" } {
      "F. Guidi:" +
      @@("version_1.html" "lambdadelta_1") +
-     "(revised <span class=\"emph delta\">2012-10</span>)." +
+     "(revised <span class=\"emph delta\">2015-01</span>)." +
      "Formal specification for the proof assistant Coq 7.3.1 (scripts)." +
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }

diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl
index 04d6cf8b9cce02994b64238163ad165092153fa7..1d00bf77e7bcc4a25cbebba143e0a4a6c52a19db 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_2.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_2.tbl
@@ -1,18 +1,20 @@
 name "documentation_2"
 
 table {
-   [ { name "ldJ2" "<span class=\"emph alpha\">J2.</span>" "" } {
+   [ { name "ldJ2a" "<span class=\"emph alpha\">J2a.</span>" "" } {
      "F. Guidi:" +
      @@("download/basic2a.pdf"
-     "The Formal System λδ Revised - Stage A: Extending the Applicability Condition") +
+     "The Formal System λδ Revised, Stage A: Extending the Applicability Condition") +
      "(<span class=\"emph gamma\">2014-11</span>)." +
      "Submitted to ACM ToCL." +
      "CoRR identifier" +
      @("http://arxiv.org/abs/1411.0154" "1411.0154") +
-     "[v1]."
+     "[v2] (revised" +
+     "<span class=\"emph gamma\">2015-03</span>)." +
+     @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldR5" "<span class=\"emph alpha\">R5.</span>" "" } {
+   [ { name "ldR2b" "<span class=\"emph alpha\">R2b.</span>" "" } {
      "F. Guidi:" +
      @@("download/cie_2010.pdf"
      "An Efficient Validation Procedure for the Formal System λδ") +
@@ -22,7 +24,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldR4" "<span class=\"emph alpha\">R4.</span>" "" } {
+   [ { name "ldR2a" "<span class=\"emph alpha\">R2a.</span>" "" } {
      "F. Guidi:" + 
      @("http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16"
      "Landau's \"Grundlagen der Analysis\" from Automath to lambda-delta") +
@@ -31,7 +33,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ] 
-   [ { name "ldP8" "<span class=\"emph alpha\">P8.</span>" "" } {
+   [ { name "ldP2c" "<span class=\"emph alpha\">P2c.</span>" "" } {
      "F. Guidi:" + 
      @@("download/ld_talk_8s.pdf"
      "The Formal System λδ and the \"Three Problems\"") +
@@ -39,7 +41,7 @@ table {
      "Presentation at University of Bologna (slides)."
      * }
    ] 
-   [ { name "ldP7" "<span class=\"emph alpha\">P7.</span>" "" } {
+   [ { name "ldP2b" "<span class=\"emph alpha\">P2b.</span>" "" } {
      "F. Guidi:" + 
      @@("download/ld_talk_7s.pdf"
      "An Efficient Validation Procedure for the Formal System λδ") +
@@ -47,7 +49,7 @@ table {
      "Presentation at CiE 2010 (slides)."
      * }
    ]
-   [ { name "ldP6" "<span class=\"emph alpha\">P6.</span>" "" } {
+   [ { name "ldP2a" "<span class=\"emph alpha\">P2a.</span>" "" } {
      "F. Guidi:" + 
      @@("download/ld_talk_6s.pdf"
      "A Validator for the Formal System λδ") +

diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl
index ec291e009dfa9b49ac0d3a1bcb72a42ee6813e19..4df01fc55267f86e75d7f11683acab5e6ea588ee 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_3.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_3.tbl
@@ -1,12 +1,13 @@
 name "documentation_3"
 
 table {
-   [ { name "ldJ4" "<span class=\"emph alpha\">J4.</span>" "" } {
+   [ { name "ldJ3a" "<span class=\"emph alpha\">J3a.</span>" "" } {
      "F. Guidi:" +
      @@("download/gda.pdf"
      "A Verified Translation of Landau's \"Grundlagen\" from Automath into a Pure Type System, via λδ") +
      "(<span class=\"emph alpha\">2015-02</span>)." +
-     "Submitted to JFR, Univerity of Bologna."
+     "Submitted to JFR, Univerity of Bologna." +
+     @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
 }

diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index 9112a8037985ab0da12e3dc852c616d779995338..05bb7c6c2cba7514f0db9c47ca2289f02a8c3728 100644 (file)
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -54,7 +54,7 @@
       (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
       The overall validation speed of the "Grundlagen der Analysis"
       increases of 34% with respect to version 0.8.1.
-      <rlink to="documentation.html#ldJ4">Documentation (J4)</rlink>.
+      <rlink to="documentation.html#ldJ3a">Documentation (J3a)</rlink>.
       [Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
       <list><item>
          The specification of Landau's "Grundlagen der Analysis"
@@ -104,7 +104,7 @@
       Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
-      <rlink to="documentation.html#ldR4">Documentation (R4)</rlink>.
+      <rlink to="documentation.html#ldR2a">Documentation (R2a)</rlink>.
       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
       <list><item>
          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>

diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml
index 3e0f1f4af776acb81355294fc4696b07c1aa2f88..46f208da9fe3e61d856f9ccaf1f55d5bb15c77e9 100644 (file)
--- a/helm/www/lambdadelta/web/home/news.ldw.xml
+++ b/helm/www/lambdadelta/web/home/news.ldw.xml
@@ -38,7 +38,7 @@
    </news>
 
    <news class="gamma" date="October 2014.">
-      <rlink to="documentation.html#ldJ2">λδ version 2A</rlink>
+      <rlink to="documentation.html#ldJ2a">λδ version 2A</rlink>
       is released.
    </news>
 
@@ -47,7 +47,7 @@
    </news>
 
    <news class="beta" date="June 2014.">
-      <rlink to="documentation.html#ldP8">First communication on λδ version 2.</rlink>
+      <rlink to="documentation.html#ldP2c">First communication on λδ version 2.</rlink>
    </news>
 
    <news class="alpha" date="December 2012.">
@@ -140,12 +140,12 @@
    </news>
 
    <news class="gamma" date="November 2006.">
-      <rlink to="documentation.html#ldR2">λδ version 1</rlink>
+      <rlink to="documentation.html#ldR1b">λδ version 1</rlink>
       is released.
    </news>
 
    <news class="beta" date="December 2005.">
-      <rlink to="documentation.html#ldP1">First communication on λδ version 1</rlink>.
+      <rlink to="documentation.html#ldP1a">First communication on λδ version 1</rlink>.
    </news>
 
    <news class="alpha" date="May 2004.">