From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 23 Jan 2016 08:51:34 +0000 (+0000)
Subject: documentation update
X-Git-Tag: make_still_working~658
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03401922e645207c7b64b52e1c4349f7951fcf71;p=helm.git

documentation update
---

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index b3830c1cd..c89fbcf38 100644
--- a/helm/www/lambdadelta/basic_1.html
+++ b/helm/www/lambdadelta/basic_1.html
@@ -823,6 +823,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 15:33:02 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 23 Jan 2016 00:45:18 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 764ecaa30..45e5d6084 100644
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -124,7 +124,7 @@
             <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">Verified Representations of Landau's "Grundlagen" in λδ and in the Calculus of Constructions</a> (<span class="emph alpha">2015-08</span>). Submitted to JFR, Univerity of Bologna. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+            <td class="ssnn top">F. Guidi: <a href="http://jfr.unibo.it/article/view/4716">Verified Representations of Landau's "Grundlagen" in the λδ Family and in the Calculus of Constructions</a> (<span class="emph alpha">2015-12</span>). In JFR 8(1), Univerity of Bologna, pp. 93-116. <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: Wed, 30 Dec 2015 15:33:02 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 23 Jan 2016 00:45:18 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib
index 403c201cd..5e80745cf 100644
--- a/helm/www/lambdadelta/download/lambdadelta.bib
+++ b/helm/www/lambdadelta/download/lambdadelta.bib
@@ -1,11 +1,16 @@
 % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadeltaJ3a,
+@article{lambdadeltaJ3a,
    author="F. {Guidi}",
-   title="{Verified Representations of Landau's ``Grundlagen'' in $\lambda\delta$ and in the Calculus of Constructions}",
+   title="{Verified Representations of Landau's ``Grundlagen'' in the $\lambda\delta$ Family and in the Calculus of Constructions}",
+   Publisher="University of Bologna",
+   address="Bologna, Italy",
+   journal="Journal of Formalized Reasoning",
+   volume="8",
+   number="1",
    year="2015",
-   month="August",
-   note="Submitted to JFR, University of Bologna (available at $<$\url{http://lambdadelta.info/}$>$)"
+   month="December",
+   pages="93-116"
 }
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt
index 403c201cd..5e80745cf 100644
--- a/helm/www/lambdadelta/download/lambdadelta.txt
+++ b/helm/www/lambdadelta/download/lambdadelta.txt
@@ -1,11 +1,16 @@
 % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadeltaJ3a,
+@article{lambdadeltaJ3a,
    author="F. {Guidi}",
-   title="{Verified Representations of Landau's ``Grundlagen'' in $\lambda\delta$ and in the Calculus of Constructions}",
+   title="{Verified Representations of Landau's ``Grundlagen'' in the $\lambda\delta$ Family and in the Calculus of Constructions}",
+   Publisher="University of Bologna",
+   address="Bologna, Italy",
+   journal="Journal of Formalized Reasoning",
+   volume="8",
+   number="1",
    year="2015",
-   month="August",
-   note="Submitted to JFR, University of Bologna (available at $<$\url{http://lambdadelta.info/}$>$)"
+   month="December",
+   pages="93-116"
 }
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
index 4e5e6b192..698d60ab5 100644
--- 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: Wed, 30 Dec 2015 15:33:02 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 23 Jan 2016 00:45:18 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 9272c2a2a..abbd7940a 100644
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -132,29 +132,29 @@
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">48</td>
+            <td class="snnn right italic cyan">54</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">66783</td>
+            <td class="snnn right italic cyan" />
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">134126</td>
+            <td class="ssnn right italic cyan">152278</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">9</td>
+            <td class="snnn right italic green">15</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">298</td>
+            <td class="snnn right italic green">328</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">307</td>
+            <td class="ssnn right italic green">343</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">47</td>
+            <td class="snsn right italic yellow">48</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">32</td>
+            <td class="snsn right italic yellow">39</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">79</td>
+            <td class="sssn right italic yellow">87</td>
           </tr>
         </tbody>
       </table>
@@ -213,6 +213,34 @@
           <tr>
             <td class="snns top capitalize italic green">multiple relocation</td>
             <td class="snns top italic green" />
+            <td class="snns top green">nstream</td>
+            <td class="snnn top green">nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )</td>
+            <td class="snnn top green">
+              <br />
+            </td>
+            <td class="snnn top green">
+              <br />
+            </td>
+            <td class="snnn top green">
+              <br />
+            </td>
+            <td class="snnn top green">
+              <br />
+            </td>
+            <td class="snnn top green">
+              <br />
+            </td>
+            <td class="ssnn top green">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic green">
+              <br />
+            </td>
+            <td class="nnns top italic green">
+              <br />
+            </td>
             <td class="snns top green">trace ( ∥?∥ )</td>
             <td class="snnn top green">trace_at ( @⦃?,?⦄ ≡ ? )</td>
             <td class="snnn top green">trace_after ( ? ⊚ ? ≡ ? )</td>
@@ -271,12 +299,8 @@
             <td class="snnn top yellow">arith ( ?^? ) ( ⫯? ) ( ⫰? )</td>
             <td class="snnn top yellow">list ( ◊ ) ( ? @ ? ) ( |?| )</td>
             <td class="snnn top yellow">list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )</td>
-            <td class="snnn top yellow">
-              <br />
-            </td>
-            <td class="ssnn top yellow">
-              <br />
-            </td>
+            <td class="snnn top yellow">stream ( ? @ ? ) ( ? ≐ ? )</td>
+            <td class="ssnn top yellow">stream_hdtl</td>
           </tr>
           <tr>
             <td class="snns top capitalize italic orange">generated logical decomposables</td>
@@ -359,6 +383,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 23 Jan 2016 00:45:18 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 11364dc30..4f198e9fd 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -291,6 +291,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 15:33:02 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 23 Jan 2016 00:45:18 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 5ac10fed3..59973f01f 100644
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -136,7 +136,7 @@
     <ul xmlns:ld="http://lambdadelta.info/" id="C7">
       <li>
       C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
-      <span class="emph alpha">ELPI: fast, Embeddable, λProlog Interpreter</span>
+      <span class="emph alpha">ELPI: Fast, Embeddable, λProlog Interpreter</span>
       (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
    </li>
     </ul>
@@ -276,6 +276,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 15:33:02 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 23 Jan 2016 00:45:18 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 13291a901..3d676d294 100644
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -105,6 +105,13 @@
     <!-- ===================================================================== -->
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="milestones">Milestones <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
     </div>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph alpha">December 2015.</span>
+        <a href="http://lambdadelta.info/documentation.html#ldJ3a">Second journal paper on λδ</a>
+      accepted for publication.
+   </li>
+    </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph gamma">December 2015.</span>
@@ -373,6 +380,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 15:33:02 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 23 Jan 2016 00:45:18 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 027d59108..2714bff80 100644
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -135,6 +135,21 @@
             <td class="snnn top capitalize italic gray">concluded</td>
             <td class="ssnn top capitalize italic gray">references</td>
           </tr>
+          <tr>
+            <td class="snns top yellow">
+              <a href="http://lambdadelta.info/specification.html#v3">Version 3</a>
+            </td>
+            <td class="snnn top yellow">"basic_3"</td>
+            <td class="snnn top yellow" />
+            <td class="snnn top yellow" />
+            <td class="snnn top yellow" />
+            <td class="snnn top yellow" />
+            <td class="snnn top yellow" />
+            <td class="snnn top yellow" />
+            <td class="ssnn top yellow">
+              <a href="http://lambdadelta.info/documentation#ldJ3a">J3a</a>
+            </td>
+          </tr>
           <tr>
             <td class="snns top orange">
               <a href="http://lambdadelta.info/specification.html#v2">Version 2</a>
@@ -228,6 +243,13 @@
       introduced in each script, is shown in parentheses (? are placeholders).
    </li>
     </ul>
+    <!-- VERSION 3 =========================================================== -->
+    <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 formal specification of λδ version 3
+      is forthcoming.
+   </div>
     <!-- VERSION 2 =========================================================== -->
     <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>
@@ -360,6 +382,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 15:33:02 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 23 Jan 2016 00:45:18 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl
index cf80e782d..b4dd848a6 100644
--- a/helm/www/lambdadelta/web/home/documentation_3.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_3.tbl
@@ -3,10 +3,10 @@ name "documentation_3"
 table {
    [ { name "ldJ3a" "<span class=\"emph alpha\">J3a.</span>" "" } {
      "F. Guidi:" +
-     @@("download/gda.pdf"
-     "Verified Representations of Landau's \"Grundlagen\" in λδ and in the Calculus of Constructions") +
-     "(<span class=\"emph alpha\">2015-08</span>)." +
-     "Submitted to JFR, Univerity of Bologna." +
+     @("http://jfr.unibo.it/article/view/4716"
+     "Verified Representations of Landau's \"Grundlagen\" in the λδ Family and in the Calculus of Constructions") +
+     "(<span class=\"emph alpha\">2015-12</span>)." +
+     "In JFR 8(1), Univerity of Bologna, pp. 93-116." +
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml
index 5110c1470..9913b2401 100644
--- a/helm/www/lambdadelta/web/home/index.ldw.xml
+++ b/helm/www/lambdadelta/web/home/index.ldw.xml
@@ -41,7 +41,7 @@
 
    <topitem name="C7">
       C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
-      <notice class="alpha">ELPI: fast, Embeddable, λProlog Interpreter</notice>
+      <notice class="alpha">ELPI: Fast, Embeddable, λProlog Interpreter</notice>
       (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
    </topitem>
 
diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml
index 966e0fa4c..2e6e14936 100644
--- a/helm/www/lambdadelta/web/home/news.ldw.xml
+++ b/helm/www/lambdadelta/web/home/news.ldw.xml
@@ -11,6 +11,11 @@
 
    <section3 name="milestones">Milestones</section3>
 
+   <news class="alpha" date="December 2015.">
+      <rlink to="documentation.html#ldJ3a">Second journal paper on λδ</rlink>
+      accepted for publication.
+   </news>
+
    <news class="gamma" date="December 2015.">
       <rlink to="implementation.html#v3">"Helena 0.8.3"</rlink> is released.
    </news>
diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index a489b47a8..969e3fd00 100644
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -44,6 +44,14 @@
       introduced in each script, is shown in parentheses (? are placeholders).
    </topitem>
 
+<!-- VERSION 3 =========================================================== -->
+
+   <subsection name="v3"><version3-icon/>λδ version 3 (proposed)</subsection>
+   <body>
+      The formal specification of λδ version 3
+      is forthcoming.
+   </body>
+
 <!-- VERSION 2 =========================================================== -->
 
    <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl
index 5b7189241..1d88064b3 100644
--- a/helm/www/lambdadelta/web/home/versions.tbl
+++ b/helm/www/lambdadelta/web/home/versions.tbl
@@ -6,6 +6,11 @@ table {
         "stage" "started" "announced" "released" "concluded"
         "references"
       ]
+   class "yellow"
+      [ @@("specification#v3" "Version 3") "\"basic_3\"" ""
+        "" "" "" "" ""
+        @@("documentation#ldJ3a" "J3a")
+      ]
    class "orange" {
       [ { @@("specification#v2" "Version 2") * }
         { "\"basic_2\"" * }